English
Characterization: a belongs to the down-compressed family 𝓓 a 𝒜 iff either a ∈ 𝒜 and s.erase a ∈ 𝒜 or a ∉ 𝒜 and a ∪ s ∈ 𝒜.
Русский
Характеризация: элемент s принадлежит down-компрессии 𝓓 a 𝒜 тогда и только тогда, когда либо a ∈ 𝒜 и s.erase a ∈ 𝒜, либо a ∉ 𝒜 и insert a s ∈ 𝒜.
LaTeX
$$$s \\in 𝓓(a,\\mathcal{A}) \\iff (s \\in \\mathcal{A} \\wedge s\\setminus\\{a\\} \\in \\mathcal{A}) \\lor (s \\notin\\mathcal{A} \\wedge a \\cup s \\in \\mathcal{A})$$$
Lean4
/-- `a` is in the down-compressed family iff it's in the original and its compression is in the
original, or it's not in the original but it's the compression of something in the original. -/
theorem mem_compression : s ∈ 𝓓 a 𝒜 ↔ s ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ s ∉ 𝒜 ∧ insert a s ∈ 𝒜 :=
by
simp_rw [compression, mem_disjUnion, mem_filter, mem_image, and_comm (a := (s ∉ 𝒜))]
refine
or_congr_right
(and_congr_left fun hs => ⟨?_, fun h => ⟨_, h, erase_insert <| insert_ne_self.1 <| ne_of_mem_of_not_mem h hs⟩⟩)
rintro ⟨t, ht, rfl⟩
rwa [insert_erase (erase_ne_self.1 (ne_of_mem_of_not_mem ht hs).symm)]
