memberSubfamily_union — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem memberSubfamily_union (a : α) (𝒜 ℬ : Finset (Finset α)) :
    (𝒜 ∪ ℬ).memberSubfamily a = 𝒜.memberSubfamily a ∪ ℬ.memberSubfamily a := by
  simp_rw [memberSubfamily, filter_union, image_union]

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