memberSubfamily_union_nonMemberSubfamily

English

The union of 𝒜.memberSubfamily a and 𝒜.nonMemberSubfamily a equals 𝒜.image (lambda s: erase s a).

Русский

Объединение 𝒜.memberSubfamily a и 𝒜.nonMemberSubfamily a эквивалентно образу 𝒜 через функцию erase с аргументом a.

LaTeX

$$$𝒜.memberSubfamily a \cup 𝒜.nonMemberSubfamily a = 𝒜.image (\lambda s. s.erase a)$$$

Lean4

theorem memberSubfamily_union_nonMemberSubfamily (a : α) (𝒜 : Finset (Finset α)) :
    𝒜.memberSubfamily a ∪ 𝒜.nonMemberSubfamily a = 𝒜.image fun s => s.erase a :=
  by
  ext s
  simp only [mem_union, mem_memberSubfamily, mem_nonMemberSubfamily, mem_image]
  constructor
  · rintro (h | h)
    · exact ⟨_, h.1, erase_insert h.2⟩
    · exact ⟨_, h.1, erase_eq_of_notMem h.2⟩
  · rintro ⟨s, hs, rfl⟩
    by_cases ha : a ∈ s
    · exact Or.inl ⟨by rwa [insert_erase ha], notMem_erase _ _⟩
    · exact Or.inr ⟨by rwa [erase_eq_of_notMem ha], notMem_erase _ _⟩

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