theorem Char.ext {a b : Char} : a.val = b.val → a = b

theorem Char.ext_iff {a b : Char} : a = b ↔ a.val = b.val

theorem Char.le_def {a b : Char} : a ≤ b ↔ a.val ≤ b.val

theorem Char.lt_def {a b : Char} : a < b ↔ a.val < b.val

theorem Char.lt_iff_val_lt_val {a b : Char} : a < b ↔ a.val < b.val

@[simp]

theorem Char.not_le {a b : Char} : ¬a ≤ b ↔ b < a

@[simp]

theorem Char.not_lt {a b : Char} : ¬a < b ↔ b ≤ a

@[simp]

theorem Char.le_refl (a : Char) : a ≤ a

@[simp]

theorem Char.lt_irrefl (a : Char) : ¬a < a

theorem Char.le_trans {a b c : Char} : a ≤ b → b ≤ c → a ≤ c

theorem Char.lt_trans {a b c : Char} : a < b → b < c → a < c

theorem Char.le_total (a b : Char) : a ≤ b ∨ b ≤ a

theorem Char.le_antisymm {a b : Char} : a ≤ b → b ≤ a → a = b

theorem Char.lt_asymm {a b : Char} (h : a < b) : ¬b < a

theorem Char.ne_of_lt {a b : Char} (h : a < b) : a ≠ b

instance Char.ltIrrefl : Std.Irrefl fun (x1 x2 : Char) => x1 < x2

instance Char.leRefl : Std.Refl fun (x1 x2 : Char) => x1 ≤ x2

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 := ⋯ }

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 := ⋯ }

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 }

instance Char.leAntisymm : Std.Antisymm fun (x1 x2 : Char) => x1 ≤ x2

def Char.notLTAntisymm : Std.Antisymm fun (x1 x2 : Char) => ¬x1 < x2

Equations

• Char.notLTAntisymm = ⋯

instance Char.ltAsymm : Std.Asymm fun (x1 x2 : Char) => x1 < x2

instance Char.leTotal : Std.Total fun (x1 x2 : Char) => x1 ≤ x2

def Char.notLTTotal : Std.Total fun (x1 x2 : Char) => ¬x1 < x2

Equations

• Char.notLTTotal = ⋯

theorem Char.utf8Size_eq (c : Char) : c.utf8Size = 1 ∨ c.utf8Size = 2 ∨ c.utf8Size = 3 ∨ c.utf8Size = 4

@[simp]

theorem Char.ofNat_toNat (c : Char) : ofNat c.toNat = c