closedBall_zero_eq_Icc'

Mathlib.Topology.MetricSpace.Pseudo.Constructions

URI: https://scilib.ai/kg/mathlib#NNReal.closedBall_zero_eq_Icc'

English

For c ∈ ℝ≥0, the closed ball with center 0 and radius c equals the interval Icc(0,c).

Русский

Замкнутый шар с центром в 0 и радиусом c равен интервалу Icc(0,c).

LaTeX

$$$\\operatorname{closedBall}(0,c)=\\mathrm{Icc}(0,c)$$$

Lean4

theorem closedBall_zero_eq_Icc' (c : ℝ≥0) : Metric.closedBall (0 : ℝ≥0) c.toReal = Set.Icc 0 c := by ext x; simp

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

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

Разделы

Аффилиация

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