toColex_sdiff_lt_toColex_sdiff' — Mathlib

English

If a and b are not in a fixed finite set s, then adding a or b to s preserves Colex-order comparison between the two resulting sets: toColex(s ∪ {a}) ≤ toColex(s ∪ {b}) iff a ≤ b.

Русский

Если a и b не принадлежит фиксированному множеству s, то добавление a или b в s сохраняет сравнение порядка Коэкса между полученными множествами: toColex(s ∪ {a}) ≤ toColex(s ∪ {b}) тогда и только тогда, когда a ≤ b.

LaTeX

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

Lean4

@[simp]
theorem toColex_sdiff_lt_toColex_sdiff' : toColex (s \ t) < toColex (t \ s) ↔ toColex s < toColex t := by
  simpa using toColex_sdiff_lt_toColex_sdiff (inter_subset_left (s₁ := s)) inter_subset_right

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