Documentation

Init.Data.Char.Lemmas

source
@[deprecated Char.ext (since := "2025-10-26")]
theorem Char.eq_of_val_eq {a b : Char} :
a.val = b.val → a = b
source
theorem Char.le_def {a b : Char} :
a ≤ b ↔ a.val ≤ b.val
source
theorem Char.lt_def {a b : Char} :
a < b ↔ a.val < b.val
source
@[deprecated Char.lt_def (since := "2025-10-26")]
theorem Char.lt_iff_val_lt_val {a b : Char} :
a < b ↔ a.val < b.val
source
@[simp]
theorem Char.not_le {a b : Char} :
¬a ≤ b ↔ b < a
source
@[simp]
theorem Char.not_lt {a b : Char} :
¬a < b ↔ b ≤ a
source
@[simp]
theorem Char.le_refl (a : Char) :
a ≤ a
source
@[simp]
theorem Char.lt_irrefl (a : Char) :
¬a < a
source
theorem Char.le_trans {a b c : Char} :
a ≤ b → b ≤ c → a ≤ c
source
theorem Char.lt_trans {a b c : Char} :
a < b → b < c → a < c
source
theorem Char.le_total (a b : Char) :
a ≤ b ∨ b ≤ a
source
theorem Char.le_antisymm {a b : Char} :
a ≤ b → b ≤ a → a = b
source
theorem Char.lt_asymm {a b : Char} (h : a < b) :
¬b < a
source
theorem Char.ne_of_lt {a b : Char} (h : a < b) :
a ≠ b
source
instance Char.ltIrrefl :
Std.Irrefl fun (x1 x2 : Char) => x1 < x2
source
instance Char.leRefl :
Std.Refl fun (x1 x2 : Char) => x1 ≤ x2
source
@[instance_reducible]
instance Char.leTrans :
Trans (fun (x1 x2 : Char) => x1 ≤ x2) (fun (x1 x2 : Char) => x1 ≤ x2) fun (x1 x2 : Char) => x1 ≤ x2
Equations
source
@[instance_reducible]
instance Char.ltTrans :
Trans (fun (x1 x2 : Char) => x1 < x2) (fun (x1 x2 : Char) => x1 < x2) fun (x1 x2 : Char) => x1 < x2
Equations
source
@[instance_reducible]
def Char.notLTTrans :
Trans (fun (x1 x2 : Char) => ¬x1 < x2) (fun (x1 x2 : Char) => ¬x1 < x2) fun (x1 x2 : Char) => ¬x1 < x2
Equations
Instances For
    source
    instance Char.leAntisymm :
    Std.Antisymm fun (x1 x2 : Char) => x1 ≤ x2
    source
    instance Char.ltTrichotomous :
    Std.Trichotomous fun (x1 x2 : Char) => x1 < x2
    source
    @[deprecated Char.ltTrichotomous (since := "2025-10-27")]
    theorem Char.notLTAntisymm :
    Std.Antisymm fun (x1 x2 : Char) => ¬x1 < x2
    source
    instance Char.ltAsymm :
    Std.Asymm fun (x1 x2 : Char) => x1 < x2
    source
    instance Char.leTotal :
    Std.Total fun (x1 x2 : Char) => x1 ≤ x2
    source
    @[deprecated Char.ltAsymm (since := "2025-08-01")]
    theorem Char.notLTTotal :
    Std.Total fun (x1 x2 : Char) => ¬x1 < x2
    source
    @[simp]
    theorem Char.ofNat_toNat (c : Char) :
    ofNat c.toNat = c
    source
    @[simp]
    theorem Char.toUInt8_val {c : Char} :
    c.val.toUInt8 = c.toUInt8
    source
    @[simp]
    theorem Char.toString_eq_singleton {c : Char} :
    c.toString = String.singleton c
    source
    @[simp]
    theorem Char.toNat_val {c : Char} :
    c.val.toNat = c.toNat
    source
    theorem Char.val_inj {c d : Char} :
    c.val = d.val ↔ c = d
    source
    theorem Char.toNat_inj {c d : Char} :
    c.toNat = d.toNat ↔ c = d
    source
    theorem Char.isDigit_iff_toNat {c : Char} :
    c.isDigit = true ↔ '0'.toNat ≤ c.toNat ∧ c.toNat ≤ '9'.toNat
    source
    @[simp]
    theorem Char.toNat_mk {val : UInt32} {h : val.isValidChar} :
    { val := val, valid := h }.toNat = val.toNat