closedBall_zero_eq_Icc — Mathlib

English

For any real c with c ≥ 0, the closed ball centered at 0 in NNReal equals Icc(0,c).

Русский

Для любого действительного c с c ≥ 0, замкнутый шар с центром в 0 в NNReal равен Icc(0,c).

LaTeX

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

Lean4

theorem closedBall_zero_eq_Icc {c : ℝ} (c_nn : 0 ≤ c) : Metric.closedBall (0 : ℝ≥0) c = Set.Icc 0 c.toNNReal :=
  by
  convert NNReal.closedBall_zero_eq_Icc' ⟨c, c_nn⟩
  simp [Real.toNNReal, c_nn]

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