cons_lt_cons — 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) \\le \\operatorname{toColex}(\\operatorname{insert} b s) \\iff a \\le b $$$$

Lean4

@[simp]
theorem cons_lt_cons (ha hb) : toColex (s.cons a ha) < toColex (s.cons b hb) ↔ a < b :=
  lt_iff_lt_of_le_iff_le' (cons_le_cons _ _) (cons_le_cons _ _)

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