English
If a family of sets f(x) is directed by inclusion, and each f(x) is r-directed, then the union over all x is r-directed.
Русский
Если семейство множеств f(x) упорядочено по включению (направлено), и каждое множество f(x) направлено относительно отношения r, то их объединение по всем x направлено относительно r.
LaTeX
$$$$\\text{DirectedOn}_r\\Bigl(\\bigcup_{x} f(x)\\Bigr).$$$$
Lean4
theorem directedOn_iUnion {r} {f : ι → Set α} (hd : Directed (· ⊆ ·) f) (h : ∀ x, DirectedOn r (f x)) :
DirectedOn r (⋃ x, f x) := by
simp only [DirectedOn, mem_iUnion, exists_imp]
exact fun a₁ b₁ fb₁ a₂ b₂ fb₂ =>
let ⟨z, zb₁, zb₂⟩ := hd b₁ b₂
let ⟨x, xf, xa₁, xa₂⟩ := h z a₁ (zb₁ fb₁) a₂ (zb₂ fb₂)
⟨x, ⟨z, xf⟩, xa₁, xa₂⟩
