nonMemberSubfamily_union — Mathlib

English

The union of nonMemberSubfamilies equals the nonMemberSubfamily of the union.

Русский

Объединение подсемейств без элемента равно подсемейству без элемента от объединения.

LaTeX

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

Lean4

theorem nonMemberSubfamily_union (a : α) (𝒜 ℬ : Finset (Finset α)) :
    (𝒜 ∪ ℬ).nonMemberSubfamily a = 𝒜.nonMemberSubfamily a ∪ ℬ.nonMemberSubfamily a :=
  filter_union _ _ _

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