insert_lt_insert — Mathlib

English

If a and b are not in s, then toColex(insert a s) < toColex(insert b s) iff a < b.

Русский

Если a и b не принадлежат s, то toColex(insert a s) < toColex(insert b s) эквивалентно a < b.

LaTeX

$$$$ \\operatorname{toColex}(\\operatorname{insert} a s) < \\operatorname{toColex}(\\operatorname{insert} b s) \\iff a < b $$$$

Lean4

theorem insert_lt_insert (ha : a ∉ s) (hb : b ∉ s) : toColex (insert a s) < toColex (insert b s) ↔ a < b := by
  rw [← cons_eq_insert _ _ ha, ← cons_eq_insert _ _ hb, cons_lt_cons]

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