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

theorem Char.ext_iff {x : Char} {y : Char} : x = y ↔ x.val = y.val

theorem Char.le_antisymm_iff {x : Char} {y : Char} : x = y ↔ x ≤ y ∧ y ≤ x

theorem Char.le_antisymm {x : Char} {y : Char} (h1 : x ≤ y) (h2 : y ≤ x) : x = y

instance instLawfulOrdChar : Batteries.LawfulOrd Char

Equations

• instLawfulOrdChar = ⋯

theorem String.csize_pos (c : Char) : 0 < String.csize c

theorem String.csize_le_4 (c : Char) : String.csize c ≤ 4