directedOn_sUnion — Mathlib

English

If a collection S of subsets of α is directed by inclusion, and every member of S is r-directed, then the union ⋃S is r-directed.

Русский

Если множество подмножеств S ⊆ P(α) упорядочено направленно по включению и каждый элемент S является направленным относительно r, то объединение ⋃S направлено относительно r.

LaTeX

$$$$\\text{DirectedOn}_r(\\bigcup\\, S).$$$$

Lean4

theorem directedOn_sUnion {r} {S : Set (Set α)} (hd : DirectedOn (· ⊆ ·) S) (h : ∀ x ∈ S, DirectedOn r x) :
    DirectedOn r (⋃₀ S) := by
  rw [sUnion_eq_iUnion]
  exact directedOn_iUnion (directedOn_iff_directed.mp hd) (fun i ↦ h i.1 i.2)

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