English
Definition: For α, a ∈ α and Finset 𝒜 ⊆ Finset α, the down-compression 𝒟 a 𝒜 is the disjoint union of those s ∈ 𝒜 with s.erase a ∈ 𝒜 and those s ∈ 𝒜.image(erase a) with s ∉ 𝒜.
Русский
Определение: для множества α, элемента a и семейства 𝒜 ⊆ Finset α, down-про compressed 𝒟 a 𝒜 — это дизъюнктное объединение всех s ∈ 𝒜, у которых s.erase a ∈ 𝒜, и всех элементов вида s.erase a, где s ∈ 𝒜 не принадлежит 𝒜.
LaTeX
$$$\\mathcal{D}(a,\\mathcal{A}) := \\{ S \\in \\mathcal{A} \\mid S\\setminus\\{a\\} \\in \\mathcal{A} \\} \\cup \\{ S' \\in \\mathcal{A}.image( erase\\ a) \\mid S' \\notin \\mathcal{A} \\}$$$
Lean4
/-- `a`-down-compressing `𝒜` means removing `a` from the elements of `𝒜` that contain it, when the
resulting Finset is not already in `𝒜`. -/
def compression (a : α) (𝒜 : Finset (Finset α)) : Finset (Finset α) :=
{s ∈ 𝒜 | erase s a ∈ 𝒜}.disjUnion ({s ∈ 𝒜.image fun s ↦ erase s a | s ∉ 𝒜}) <|
disjoint_left.2 fun _s h₁ h₂ ↦ (mem_filter.1 h₂).2 (mem_filter.1 h₁).1
