toColex_sdiff_le_toColex_sdiff' — Mathlib

English

Removing a common subset preserves strict Colex order: if u ⊆ s and u ⊆ t, then toColex(s \\ u) < toColex(t \\ u) iff toColex(s) < toColex(t).

Русский

Удаление общей подмножности сохраняет строгий порядок Коэкса: если u ⊆ s и u ⊆ t, то toColex(s \\ u) < toColex(t \\ u) тогда и только тогда, когда toColex(s) < toColex(t).

LaTeX

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

Lean4

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

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