English
If a directedOn family c of sets is such that every member is convex, then the union ⋃₀ c is convex.
Русский
Если семейство c, направленное по включению, состоит из выпуклых множеств, то их объединение выпукло.
LaTeX
$$$\text{DirectedOn } (\cdot \subseteq \cdot)\ c \to (\forall A \in c, Convex 𝕜 A) \to Convex 𝕜 (\bigcup c)$$$
Lean4
theorem convex_sUnion {c : Set (Set E)} (hdir : DirectedOn (· ⊆ ·) c) (hc : ∀ ⦃A : Set E⦄, A ∈ c → Convex 𝕜 A) :
Convex 𝕜 (⋃₀ c) := by
rw [sUnion_eq_iUnion]
exact (directedOn_iff_directed.1 hdir).convex_iUnion fun A => hc A.2