SemVer.Lemmas

In this file, theorems are provided that assert that the less-than (<) relations for the types used to define version numbers are transitive, i.e. that a < c results from a < b ∧ b < c.

@[simp]

theorem NonEmptyList.inj_incr {α : Type} [LT α] (a b : NonEmptyList α) : a < b ↔ a.val < b.val

Ensures that the canonical injection

fun {α} a ↦ a.val : {α : Type} → NonEmptyList α → List α

is strictly increasing under the respective <-relations.

@[simp]

theorem NonEmptyList.lt_trans {α : Type} [LT α] [g : Trans (fun (x1 x2 : α) => x1 < x2) (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : α) => x1 < x2] {a b c : NonEmptyList α} (h1 : a < b) (h2 : b < c) : a < c

Asserts that < is a transitive relation inNonEmptyList α if the underlying < on α has the same property.

@[implicit_reducible]

instance NonEmptyList.instTransLt {α : Type} [LT α] [Trans (fun (x1 x2 : α) => x1 < x2) (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : α) => x1 < x2] : Trans (fun (x1 x2 : NonEmptyList α) => x1 < x2) (fun (x1 x2 : NonEmptyList α) => x1 < x2) fun (x1 x2 : NonEmptyList α) => x1 < x2

Equations

• NonEmptyList.instTransLt = { trans := ⋯ }

@[simp]

theorem NonEmptyString.inj_incr (a b : NonEmptyString) : a < b ↔ a.val < b.val

Assert that the canonical injection

fun a ↦ a.val : NonEmptyString → String

is a strictly increasing function under the respective <-relations.

@[simp]

theorem NonEmptyString.lt_trans {a b c : NonEmptyString} (h1 : a < b) (h2 : b < c) : a < c

Asserts that < is transitive on NonEmptyString.

@[implicit_reducible]

instance NonEmptyString.instTransLt : Trans (fun (x1 x2 : NonEmptyString) => x1 < x2) (fun (x1 x2 : NonEmptyString) => x1 < x2) fun (x1 x2 : NonEmptyString) => x1 < x2

Equations

• NonEmptyString.instTransLt = { trans := ⋯ }

@[simp]

theorem Digits.lt_trans {a b c : Digits} (h1 : a < b) (h2 : b < c) : a < c

Asserts that < is transitive on Digits.

@[implicit_reducible]

instance Digits.instTransLt : Trans (fun (x1 x2 : Digits) => x1 < x2) (fun (x1 x2 : Digits) => x1 < x2) fun (x1 x2 : Digits) => x1 < x2

Equations

• Digits.instTransLt = { trans := ⋯ }

@[simp]

theorem NumIdent.lt_trans {a b c : NumIdent} (h1 : a < b) (h2 : b < c) : a < c

Ensures that < is transitive on NumIdent.

@[implicit_reducible]

instance NumIdent.instTransLt : Trans (fun (x1 x2 : NumIdent) => x1 < x2) (fun (x1 x2 : NumIdent) => x1 < x2) fun (x1 x2 : NumIdent) => x1 < x2

Equations

• NumIdent.instTransLt = { trans := ⋯ }

@[simp]

theorem Ident.lt_trans {a b c : Ident} (h1 : a < b) (h2 : b < c) : a < c

Ensures that < is transitive on Ident.

@[implicit_reducible]

instance Ident.instTransLt : Trans (fun (x1 x2 : Ident) => x1 < x2) (fun (x1 x2 : Ident) => x1 < x2) fun (x1 x2 : Ident) => x1 < x2

Equations

• Ident.instTransLt = { trans := ⋯ }

@[simp]

theorem AlphanumIdent.lt_trans {a b c : AlphanumIdent} (h1 : a < b) (h2 : b < c) : a < c

Ensures that < is transitive on AlphanumIdent.

@[implicit_reducible]

instance AlphanumIdent.instTransLt : Trans (fun (x1 x2 : AlphanumIdent) => x1 < x2) (fun (x1 x2 : AlphanumIdent) => x1 < x2) fun (x1 x2 : AlphanumIdent) => x1 < x2

Equations

• AlphanumIdent.instTransLt = { trans := ⋯ }

@[simp]

theorem PreRelIdent.lt_trans {a b c : PreRelIdent} (h1 : a < b) (h2 : b < c) : a < c

Ensures that < is transitive on PreRelIdent.

@[implicit_reducible]

instance PreRelIdent.instTransLt : Trans (fun (x1 x2 : PreRelIdent) => x1 < x2) (fun (x1 x2 : PreRelIdent) => x1 < x2) fun (x1 x2 : PreRelIdent) => x1 < x2

Equations

• PreRelIdent.instTransLt = { trans := ⋯ }

@[simp]

theorem DotSepPreRelIdents.lt_trans {a b c : DotSepPreRelIdents} (h1 : a < b) (h2 : b < c) : a < c

Ensures that < is transitive on DotSepPreRelIdents.

@[implicit_reducible]

instance DotSepPreRelIdents.instTransLt : Trans (fun (x1 x2 : DotSepPreRelIdents) => x1 < x2) (fun (x1 x2 : DotSepPreRelIdents) => x1 < x2) fun (x1 x2 : DotSepPreRelIdents) => x1 < x2

Equations

• DotSepPreRelIdents.instTransLt = { trans := ⋯ }

@[simp]

theorem VersionCore.lt_trans {a b c : VersionCore} (h1 : a < b) (h2 : b < c) : a < c

Ensures that < is transitive on VersionCore.

@[implicit_reducible]

instance VersionCore.instTransLt : Trans (fun (x1 x2 : VersionCore) => x1 < x2) (fun (x1 x2 : VersionCore) => x1 < x2) fun (x1 x2 : VersionCore) => x1 < x2

Equations

• VersionCore.instTransLt = { trans := ⋯ }

@[simp]

theorem Version.ltPreRelease_trans {a b c : Version} (h1 : a.ltPreRelease b = true) (h2 : b.ltPreRelease c = true) : a.ltPreRelease c = true

Lemma asserting that Version.ltPreRelease is transitive.

@[simp]

theorem Version.lt_trans {a b c : Version} (h1 : a < b) (h2 : b < c) : a < c

Ensures that < is transitive on Version.

@[implicit_reducible]

instance Version.instTransLt : Trans (fun (x1 x2 : Version) => x1 < x2) (fun (x1 x2 : Version) => x1 < x2) fun (x1 x2 : Version) => x1 < x2

Equations

• Version.instTransLt = { trans := ⋯ }