metricSpaceEMetricBall — Mathlib

English

Every ball in an extended metric space carries a metric space structure.

Русский

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

LaTeX

$$$\text{MetricSpace}(\text{ball } a r)$$$

Lean4

/-- Each ball in an extended metric space gives us a metric space, as the edist
is everywhere finite. -/
def metricSpaceEMetricBall (a : β) (r : ℝ≥0∞) : MetricSpace (ball a r) :=
  EMetricSpace.toMetricSpace edist_ne_top_of_mem_ball

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