toColex_sdiff_le_toColex_sdiff — Mathlib

English

Removing the same finite subset u from both s and t does not change their Colex order: s \\ u ≤ t \\ u iff s ≤ t.

Русский

Удаление одной и той же подмножности u из двух множеств s и t не изменяет их порядок Коэкса: s \\ u ≤ t \\ u эквивалентно s ≤ t.

LaTeX

$$$$ toColex(s \\ u) \\le toColex(t \\ u) \\iff toColex(s) \\le toColex(t) $$$$

Lean4

/-- The colexigraphic order is insensitive to removing the same elements from both sets. -/
theorem toColex_sdiff_le_toColex_sdiff (hus : u ⊆ s) (hut : u ⊆ t) :
    toColex (s \ u) ≤ toColex (t \ u) ↔ toColex s ≤ toColex t := by
  simp_rw [toColex_le_toColex, ← and_imp, ← and_assoc, ← mem_sdiff,
    sdiff_sdiff_sdiff_cancel_right (show u ≤ s from hus), sdiff_sdiff_sdiff_cancel_right (show u ≤ t from hut)]

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