mem_memberSubfamily — Mathlib

English

(A ∩ B).memberSubfamily a = A.memberSubfamily a ∩ B.memberSubfamily a.

Русский

(𝒜 ∩ ℬ).memberSubfamily a = 𝒜.memberSubfamily a ∩ ℬ.memberSubfamily a.

LaTeX

$$$ (𝒜 \cap ℬ).memberSubfamily(a) = 𝒜.memberSubfamily(a) \cap ℬ.memberSubfamily(a) $$$

Lean4

@[simp]
theorem mem_memberSubfamily : s ∈ 𝒜.memberSubfamily a ↔ insert a s ∈ 𝒜 ∧ a ∉ s :=
  by
  simp_rw [memberSubfamily, mem_image, mem_filter]
  refine ⟨?_, fun h => ⟨insert a s, ⟨h.1, by simp⟩, erase_insert h.2⟩⟩
  rintro ⟨s, ⟨hs1, hs2⟩, rfl⟩
  rw [insert_erase hs2]
  exact ⟨hs1, notMem_erase _ _⟩

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