mkMetric_top — Mathlib

English

The metric outer measure built by mkMetric with the constant ∞ function is the top element of the outer measure lattice.

Русский

Метрика-outer measure, построенная как константа ∞, является наивысшим элементом решётки внешних мер.

LaTeX

$$mkMetric_top : (mkMetric (fun _ => ∞) ) = ⊤$$

Lean4

@[simp]
theorem mkMetric_top : (mkMetric (fun _ => ∞ : ℝ≥0∞ → ℝ≥0∞) : OuterMeasure X) = ⊤ :=
  by
  simp_rw [mkMetric, mkMetric', mkMetric'.pre, extend_top, boundedBy_top, eq_top_iff]
  rw [le_iSup_iff]
  intro b hb
  simpa using hb ⊤

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