English
If S is a directed family of subsets of α, and each S-element is pairwise-related by r, then the union over all s ∈ S is pairwise-related by r.
Русский
Если S образована направленным семейством подмножеств α, и каждое подмножество удовлетворяет свойству pairwise по отношению r, тогда объединение по всем s ∈ S сохраняет свойство pairwise по r.
LaTeX
$$$$ (\\bigcup_{s ∈ S} s).\\text{Pairwise } r. $$$$
Lean4
theorem pairwise_iUnion₂ {S : Set (Set α)} (hd : DirectedOn (· ⊆ ·) S) (r : α → α → Prop) (h : ∀ s ∈ S, s.Pairwise r) :
(⋃ s ∈ S, s).Pairwise r :=
by
simp only [Set.Pairwise, Set.mem_iUnion, exists_prop, forall_exists_index, and_imp]
intro x S hS hx y T hT hy hne
obtain ⟨U, hU, hSU, hTU⟩ := hd S hS T hT
exact h U hU (hSU hx) (hTU hy) hne
