English
Let S be a family of subsets of E directed by inclusion. If every member s in S is strictly convex, then the union ⋃₀ S is strictly convex.
Русский
Пусть S — семейство подмножеств пространства E, направленное по включению. Если каждый элемент s ∈ S является строго выпуклым, то объединение ⋃₀ S также строго выпукло.
LaTeX
$$$\left( \forall s_1,s_2 \in S, \exists t \in S: s_1 \subseteq t \land s_2 \subseteq t \right) \land \left( \forall s \in S, \StrictConvex 𝕜 s \right) \Rightarrow \StrictConvex 𝕜 (⋃₀ S). $$$
Lean4
theorem strictConvex_sUnion {S : Set (Set E)} (hdir : DirectedOn (· ⊆ ·) S) (hS : ∀ s ∈ S, StrictConvex 𝕜 s) :
StrictConvex 𝕜 (⋃₀ S) := by
rw [sUnion_eq_iUnion]
exact (directedOn_iff_directed.1 hdir).strictConvex_iUnion fun s => hS _ s.2
