ball_normSeminorm — Mathlib

English

The ball defined by the normSeminorm coincides with the standard metric ball: for every x and r, the set {y : (normSeminorm 𝕜 E)(y−x) < r} equals {y : ||y−x|| < r}.

Русский

Шар, определённый нормеSeminorm, совпадает с обычным метрическим шаром: для всех x и r множество {y : (normSeminorm 𝕜 E)(y−x) < r} равно {y : ||y−x|| < r}.

LaTeX

$$$\text{(normSeminorm } 𝕜 E)\text{.ball} = \text{Metric.ball}.$$$

Lean4

@[simp]
theorem ball_normSeminorm : (normSeminorm 𝕜 E).ball = Metric.ball :=
  by
  ext x r y
  simp only [Seminorm.mem_ball, Metric.mem_ball, coe_normSeminorm, dist_eq_norm]

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