memberSubfamily_inter — 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

theorem memberSubfamily_inter (a : α) (𝒜 ℬ : Finset (Finset α)) :
    (𝒜 ∩ ℬ).memberSubfamily a = 𝒜.memberSubfamily a ∩ ℬ.memberSubfamily a :=
  by
  unfold memberSubfamily
  rw [filter_inter_distrib, image_inter_of_injOn _ _ ((erase_injOn' _).mono _)]
  simp

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