Documentation

Init.Data.Char.Lemmas

source
theorem Char.ext {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
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 Char.leTrans :
Trans (fun (x1 x2 : Char) => x1 ≤ x2) (fun (x1 x2 : Char) => x1 ≤ x2) fun (x1 x2 : Char) => x1 ≤ x2
Equations
source
instance Char.ltTrans :
Trans (fun (x1 x2 : Char) => x1 < x2) (fun (x1 x2 : Char) => x1 < x2) fun (x1 x2 : Char) => x1 < x2
Equations
source
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
    def Char.notLTAntisymm :
    Std.Antisymm fun (x1 x2 : Char) => ¬x1 < x2
    Equations
    Instances For
      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
      def Char.notLTTotal :
      Std.Total fun (x1 x2 : Char) => ¬x1 < x2
      Equations
      Instances For
        source
        theorem Char.utf8Size_eq (c : Char) :
        c.utf8Size = 1 ∨ c.utf8Size = 2 ∨ c.utf8Size = 3 ∨ c.utf8Size = 4
        source
        @[simp]
        theorem Char.ofNat_toNat (c : Char) :
        Char.ofNat c.toNat = c
        source
        @[reducible, inline, deprecated Char.utf8Size (since := "2024-06-04")]
        abbrev String.csize (c : Char) :
        Nat
        Equations
        Instances For