le_iff_toList_le — Mathlib

English

String order is determined by the order of their character lists: s1 ≤ s2 iff s1.toList ≤ s2.toList.

Русский

Порядок строк задаётся порядком их списков символов: s1 ≤ s2 эквивалентно s1.toList ≤ s2.toList.

LaTeX

$$$ s_1 \le s_2 \iff s_1.toList \le s_2.toList. $$$

Lean4

@[simp]
theorem le_iff_toList_le {s₁ s₂ : String} : s₁ ≤ s₂ ↔ s₁.toList ≤ s₂.toList :=
  (not_congr lt_iff_toList_lt).trans not_lt

Похожие утверждения