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

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

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

@[simp]

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

@[simp]

theorem Char.not_lt {a : Char} {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 : Char} {b : Char} {c : Char} : a ≤ b → b ≤ c → a ≤ c

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

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

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

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

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) : Char.ofNat c.toNat = c

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

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

@[reducible, inline, deprecated Char.utf8Size]

abbrev String.csize (c : Char) : Nat

Equations

• String.csize = Char.utf8Size