tendsto_pre — Mathlib

English

For an outer measure pre m r s, as r decreases to 0 from above, the premeasure tends to the metric mkMetric' m s; i.e., Tendsto (r ↦ pre m r s) to mkMetric' m s along 𝓝[>]0.

Русский

При уменьшении r до нуля сверху, предмера pre m r s сходится к метрике mkMetric' m s: Tendsto (r ↦ pre m r s) к mkMetric' m s при 𝓝[>]0.

LaTeX

$$$$ \mathrm{Tendsto}\big( \lambda r, \mathrm{pre}\, m\, r\, s \big) \, (\mathcal{N}_{(0,\infty)}) \, (\mathcal{N}\, (\mathrm{mkMetric}'\, m\, s)). $$$$

Lean4

theorem tendsto_pre (m : Set X → ℝ≥0∞) (s : Set X) : Tendsto (fun r => pre m r s) (𝓝[>] 0) (𝓝 <| mkMetric' m s) :=
  by
  rw [← map_coe_Ioi_atBot, tendsto_map'_iff]
  simp only [mkMetric', OuterMeasure.iSup_apply, iSup_subtype']
  exact tendsto_atBot_iSup fun r r' hr => mono_pre _ hr _

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