source
theorem Char.ext {a b : Char} :
a.val = b.val → a = b
source
theorem Char.ext_iff {a b : Char} :
a = b ↔ a.val = b.val
source
theorem Char.le_def {a b : Char} :
a ≤ b ↔ a.val ≤ b.val
source
theorem Char.lt_def {a b : Char} :
a < b ↔ a.val < b.val
source
theorem Char.lt_iff_val_lt_val {a b : Char} :
a < b ↔ a.val < b.val
source
@[simp]
theorem Char.not_le {a b : Char} :
¬a ≤ b ↔ b < a
source
@[simp]
theorem Char.not_lt {a b : Char} :
¬a < b ↔ b ≤ a
source
@[simp]
theorem Char.le_refl (a : Char) :
a ≤ a
source
@[simp]
theorem Char.lt_irrefl (a : Char) :
¬a < a
source
theorem Char.le_trans {a b c : Char} :
a ≤ b → b ≤ c → a ≤ c
source
theorem Char.lt_trans {a b c : Char} :
a < b → b < c → a < c
source
theorem Char.le_total (a b : Char) :
a ≤ b ∨ b ≤ a
source
theorem Char.le_antisymm {a b : Char} :
a ≤ b → b ≤ a → a = b
source
theorem Char.lt_asymm {a b : Char} (h : a < b) :
¬b < a
source
theorem Char.ne_of_lt {a b : Char} (h : a < b) :
a ≠ b
source
instance Char.ltIrrefl :
Std.Irrefl fun (x1 x2 : Char) => x1 < x2
source
instance Char.leRefl :
Std.Refl fun (x1 x2 : Char) => x1 ≤ x2
source
instance Char.leTrans :
Trans (fun (x1 x2 : Char) => x1 ≤ x2) (fun (x1 x2 : Char) => x1 ≤ x2) fun (x1 x2 : Char) => x1 ≤ x2
Equations

- Char.leTrans = { trans := ⋯ }

source
instance Char.ltTrans :
Trans (fun (x1 x2 : Char) => x1 < x2) (fun (x1 x2 : Char) => x1 < x2) fun (x1 x2 : Char) => x1 < x2
Equations

- Char.ltTrans = { trans := ⋯ }

source
def Char.notLTTrans :
Trans (fun (x1 x2 : Char) => ¬x1 < x2) (fun (x1 x2 : Char) => ¬x1 < x2) fun (x1 x2 : Char) => ¬x1 < x2
Equations

- Char.notLTTrans = { trans := @Char.notLTTrans._proof_1✝ }

Instances For

source
instance Char.leAntisymm :
Std.Antisymm fun (x1 x2 : Char) => x1 ≤ x2
source
def Char.notLTAntisymm :
Std.Antisymm fun (x1 x2 : Char) => ¬x1 < x2
Equations

- Char.notLTAntisymm = ⋯

Instances For

source
instance Char.ltAsymm :
Std.Asymm fun (x1 x2 : Char) => x1 < x2
source
instance Char.leTotal :
Std.Total fun (x1 x2 : Char) => x1 ≤ x2
source
@[deprecated Char.ltAsymm (since := "2025-08-01")]
def Char.notLTTotal :
Std.Total fun (x1 x2 : Char) => ¬x1 < x2
Equations

- Char.notLTTotal = ⋯

Instances For

source
@[simp]
theorem Char.ofNat_toNat (c : Char) :
ofNat c.toNat = c