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

instance instLawfulOrdChar : Batteries.LawfulOrd Char

@[deprecated Char.utf8Size_pos (since := "2024-06-11")]

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

Alias of Char.utf8Size_pos.

@[deprecated Char.utf8Size_le_four (since := "2024-06-11")]

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

Alias of Char.utf8Size_le_four.