convex_sInter

Mathlib.Analysis.Convex.Basic

URI: https://scilib.ai/kg/mathlib#convex_sInter

English

The intersection over a set of convex sets is convex.

Русский

Пересечение множества выпуклых множеств выпукло.

LaTeX

$$$\forall S:\ Set(Set E),\ (\forall s\in S, \mathrm{Convex } 𝕜 s) \Rightarrow \mathrm{Convex } 𝕜 (\bigcap S)$$$

Lean4

theorem convex_sInter {S : Set (Set E)} (h : ∀ s ∈ S, Convex 𝕜 s) : Convex 𝕜 (⋂₀ S) := fun _ hx =>
  starConvex_sInter fun _ hs => h _ hs <| hx _ hs

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru