source
theorem String.data_eq_of_eq {a b : String} (h : a = b) :
a.data = b.data
source
theorem String.ne_of_data_ne {a b : String} (h : a.data ≠ b.data) :
a ≠ b
source
@[simp]
theorem String.not_le {a b : String} :
¬a ≤ b ↔ b < a
source
@[simp]
theorem String.not_lt {a b : String} :
¬a < b ↔ b ≤ a
source
@[simp]
theorem String.le_refl (a : String) :
a ≤ a
source
@[simp]
theorem String.lt_irrefl (a : String) :
¬a < a
source
theorem String.le_trans {a b c : String} :
a ≤ b → b ≤ c → a ≤ c
source
theorem String.lt_trans {a b c : String} :
a < b → b < c → a < c
source
theorem String.le_total (a b : String) :
a ≤ b ∨ b ≤ a
source
theorem String.le_antisymm {a b : String} :
a ≤ b → b ≤ a → a = b
source
theorem String.lt_asymm {a b : String} (h : a < b) :
¬b < a
source
theorem String.ne_of_lt {a b : String} (h : a < b) :
a ≠ b
source
instance String.instIsLinearOrder :
Std.IsLinearOrder String
source
instance String.instLawfulOrderLT :
Std.LawfulOrderLT String