strictConvex_iUnion — Mathlib

English

The union of directed family of strictly convex sets is strictly convex.

Русский

Объединение направленной семейства строго выпуклых множеств есть строго выпукло.

LaTeX

$$$\text{Directed }(s_i) \Rightarrow \text{StrictConvex}(\bigcup_i s_i)$$$

Lean4

theorem strictConvex_iUnion {ι : Sort*} {s : ι → Set E} (hdir : Directed (· ⊆ ·) s)
    (hs : ∀ ⦃i : ι⦄, StrictConvex 𝕜 (s i)) : StrictConvex 𝕜 (⋃ i, s i) :=
  by
  rintro x hx y hy hxy 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 interior_mono (subset_iUnion s k) (hs (hik hx) (hjk hy) hxy ha hb hab)

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