cons_le_cons — Mathlib

English

If a,b not in s, then toColex(s ∪ {a}) < toColex(s ∪ {b}) iff a < b.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem cons_le_cons (ha hb) : toColex (s.cons a ha) ≤ toColex (s.cons b hb) ↔ a ≤ b :=
  by
  obtain rfl | hab := eq_or_ne a b
  · simp
  classical
    rw [← toColex_sdiff_le_toColex_sdiff', cons_sdiff_cons hab, cons_sdiff_cons hab.symm, singleton_le_singleton]

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