le_iff_sdiff_subset_lowerClosure — Mathlib

English

For Colex elements s,t, the order relation is captured by a set-theoretic condition: s ≤ t holds exactly when every element of s not in t is below an element of t not in s.

Русский

Для элементов Коэкса s, t выполняется s ≤ t тогда, когда каждый элемент s, не входящий в t, лежит ниже некоторого элемента t, не входящего в s.

LaTeX

$$$$ s \\le t \\iff (\\uparrow(\\operatorname{ofColex} s) \\setminus \\uparrow(\\operatorname{ofColex} t)) \\subseteq \\operatorname{lowerClosure}(\\uparrow(\\operatorname{ofColex} t) \\setminus \\uparrow(\\operatorname{ofColex} s)) $$$$

Lean4

theorem le_iff_sdiff_subset_lowerClosure {s t : Colex (Finset α)} :
    s ≤ t ↔ (↑(ofColex s) : Set α) \ ↑(ofColex t) ⊆ lowerClosure (↑(ofColex t) \ ↑(ofColex s) : Set α) := by
  simp [le_def, Set.subset_def, and_assoc]

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