closedBall_normSeminorm — Mathlib

English

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

Русский

Замкнутый шар, задаваемый normSeminorm, совпадает с обычным метрическим замкнутым шаром.

LaTeX

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

Lean4

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

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