English
If f: κ → Set α and the family g n is directed by inclusion, then (⋃ n, g n).PairwiseDisjoint f iff ∀ n, (g n).PairwiseDisjoint f.
Русский
Если f: κ → Set α и семейство g n направлено по включению, то ⋃ n g n попарно непересекается с f тогда как ∀ n, (g n) попарно непересекается с f.
LaTeX
$$$$\text{Directed } (· \subseteq \cdot) g \Rightarrow (\bigcup_n g_n)\text{PairwiseDisjoint } f \iff \forall n, (g_n)\text{PairwiseDisjoint } f.$$$$
Lean4
theorem pairwise_iUnion {f : κ → Set α} (h : Directed (· ⊆ ·) f) : (⋃ n, f n).Pairwise r ↔ ∀ n, (f n).Pairwise r :=
by
constructor
· intro H n
exact Pairwise.mono (subset_iUnion _ _) H
· intro H i hi j hj hij
rcases mem_iUnion.1 hi with ⟨m, hm⟩
rcases mem_iUnion.1 hj with ⟨n, hn⟩
rcases h m n with ⟨p, mp, np⟩
exact H p (mp hm) (np hn) hij
