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

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

instance instLawfulOrdChar : Batteries.LawfulOrd Char

@[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.