erase_le_erase — Mathlib

English

If a,b ∈ s, then removing a or b from s compares oppositely: toColex(s.erase a) ≤ toColex(s.erase b) iff b ≤ a.

Русский

Если a,b ∈ s, то удаление a или b из s даёт обратное сравнение: toColex(s.erase a) ≤ toColex(s.erase b) ⇔ b ≤ a.

LaTeX

$$$$ \\operatorname{toColex}(s\\setminus a) \\le \\operatorname{toColex}(s\\setminus b) \\iff b \\le a $$$$

Lean4

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

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