pairwiseDisjoint_iUnion — Mathlib

English

If g is directed by inclusion, then (⋃ n, g n).PairwiseDisjoint f is equivalent to ∀ n, (g n).PairwiseDisjoint f.

Русский

Если g направлено по включению, то (⋃ n, g n).PairwiseDisjoint f эквивалентно ∀ n, (g n).PairwiseDisjoint f.

LaTeX

$$$$\text{Directed } (\cdot) g \Rightarrow (\bigcup_n g_n)\text{PairwiseDisjoint } f \iff \forall n, (g_n)\text{PairwiseDisjoint } f.$$$$

Lean4

theorem pairwiseDisjoint_iUnion {g : ι' → Set ι} (h : Directed (· ⊆ ·) g) :
    (⋃ n, g n).PairwiseDisjoint f ↔ ∀ ⦃n⦄, (g n).PairwiseDisjoint f :=
  pairwise_iUnion h

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