English
Let 𝒜 be a finite family of finite subsets of α and let a ∈ α with a not contained in any member of 𝒜. Then the image of 𝒜 under the operation insert a, taken with respect to the element a, recovers 𝒜: (𝒜.image insert a).memberSubfamily a = 𝒜.
Русский
Пусть 𝒜 — конечное семейство конечных подмножеств α и пусть a ∈ α так, что a не принадлежит ни одному элементу 𝒜. Тогда образ 𝒜 при вставке a с последующим выбором подсемейства, содержащего a, восстанавливает 𝒜: (𝒜.image insert a).memberSubfamily a = 𝒜.
LaTeX
$$$\\bigl(\\mathcal{A}.image( insert\ \ a)\\bigr).{\\rm memberSubfamily}\ a = \\mathcal{A}$$$
Lean4
theorem memberSubfamily_image_insert (h𝒜 : ∀ s ∈ 𝒜, a ∉ s) : (𝒜.image <| insert a).memberSubfamily a = 𝒜 :=
by
ext s
simp only [mem_memberSubfamily, mem_image]
refine ⟨?_, fun hs ↦ ⟨⟨s, hs, rfl⟩, h𝒜 _ hs⟩⟩
rintro ⟨⟨t, ht, hts⟩, hs⟩
rwa [← insert_erase_invOn.2.injOn (h𝒜 _ ht) hs hts]
