erase_lt_erase — Mathlib

English

If a,b ∈ s, then toColex(s.erase a) < toColex(s.erase b) iff b < a.

Русский

Если a,b ∈ s, то toColex(s.erase a) < toColex(s.erase b) тогда и только тогда, когда b < a.

LaTeX

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

Lean4

theorem erase_lt_erase (ha : a ∈ s) (hb : b ∈ s) : toColex (s.erase a) < toColex (s.erase b) ↔ b < a :=
  lt_iff_lt_of_le_iff_le' (erase_le_erase hb ha) (erase_le_erase ha hb)

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