convex_sUnion — Mathlib

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

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