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

@[deprecated Char.utf8Size_pos]

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

Alias of Char.utf8Size_pos.

@[deprecated Char.utf8Size_le_four]

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

Alias of Char.utf8Size_le_four.