convex_iUnion — Mathlib

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⟩

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