image_insert_memberSubfamily — Mathlib

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]

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