ball_zero_eq_Ico — Mathlib

English

For c ∈ ℝ≥0, the ball centered at 0 of radius c in NNReal equals Ico(0,c).

Русский

Шар с центром в 0 и радиусом c в NNReal равен интервалу Ico(0,c).

LaTeX

$$$\\operatorname{Metric.ball}(0, c)=\\mathrm{Ico}(0,c)$$$

Lean4

theorem ball_zero_eq_Ico (c : ℝ) : Metric.ball (0 : ℝ≥0) c = Set.Ico 0 c.toNNReal :=
  by
  by_cases c_pos : 0 < c
  · convert NNReal.ball_zero_eq_Ico' ⟨c, c_pos.le⟩
    simp [Real.toNNReal, c_pos.le]
  simp [not_lt.mp c_pos]

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