convex_closedBall

Mathlib.Analysis.Normed.Module.Convex

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

← MathLib Explorer

English

The closed ball is convex.

Русский

Замкнутый шар выпукл.

LaTeX

$$Convex Real (Metric.closedBall a r)$$

Lean4

theorem convex_closedBall (a : E) (r : ℝ) : Convex ℝ (Metric.closedBall a r) := by
  simpa only [Metric.closedBall, sep_univ] using (convexOn_univ_dist a).convex_le r

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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