ball_eq_ball — Mathlib

English

The uniform space ball with the metric-implied set equals the metric open ball: UniformSpace.ball x {p | dist p.2 p.1 < ε} = Metric.ball x ε.

Русский

Универсальный шар вокруг x с множества, задаваемого через расстояние, совпадает с метрическим открытым шаром: UniformSpace.ball x {p | dist p.2 p.1 < ε} = Metric.ball x ε.

LaTeX

$$$ \mathrm{UniformSpace.ball}(x, \{ p \mid dist(p_2,p_1) < \varepsilon \}) = \mathrm{Metric.ball}(x, \varepsilon) $$$

Lean4

theorem ball_eq_ball (ε : ℝ) (x : α) : UniformSpace.ball x {p | dist p.2 p.1 < ε} = Metric.ball x ε :=
  rfl

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