English
The image of the memberSubfamily a under the insertion of a yields the subset of 𝒜 consisting of those members that contain a: (𝒜.memberSubfamily a).image (insert a) = {s ∈ 𝒜 | a ∈ s}.
Русский
Образ подсемейства, содержающего a, под операцией вставки a равен подмножеству 𝒜, состоящему из множеств, содержащих a.
LaTeX
$$$ (\\mathcal{A}.\\mathrm{memberSubfamily}\\ a).image( insert\\ a ) = \\{ s \\in \\mathcal{A} \\mid a \\in s \\}$$$
Lean4
theorem image_insert_memberSubfamily (𝒜 : Finset (Finset α)) (a : α) :
(𝒜.memberSubfamily a).image (insert a) = {s ∈ 𝒜 | a ∈ s} :=
by
ext s
simp only [mem_memberSubfamily, mem_image, mem_filter]
refine ⟨?_, fun ⟨hs, ha⟩ ↦ ⟨erase s a, ⟨?_, notMem_erase _ _⟩, insert_erase ha⟩⟩
· rintro ⟨s, ⟨hs, -⟩, rfl⟩
exact ⟨hs, mem_insert_self _ _⟩
· rwa [insert_erase ha]