English
The union of a directed family of convex sets is convex.
Русский
Объединение направленной системы выпуклых множеств выпукло.
LaTeX
$$$(\forall i,\ Convex 𝕜 (s i)) \to \Convex 𝕜 \left( \bigcup_{i} s i \right)$$$
Lean4
theorem convex_iUnion {ι : Sort*} {s : ι → Set E} (hdir : Directed (· ⊆ ·) s) (hc : ∀ ⦃i : ι⦄, Convex 𝕜 (s i)) :
Convex 𝕜 (⋃ i, s i) := by
rintro x hx y hy a b ha hb hab
rw [mem_iUnion] at hx hy ⊢
obtain ⟨i, hx⟩ := hx
obtain ⟨j, hy⟩ := hy
obtain ⟨k, hik, hjk⟩ := hdir i j
exact ⟨k, hc (hik hx) (hjk hy) ha hb hab⟩