isTightMeasureSet_of_tendsto_measure_norm_gt

English

A finite measure μ on a complete, second-countable space is tight.

Русский

Конечная мера μ на заполненном, счетном по базису пространстве плотна.

LaTeX

$$IsTightMeasureSet { μ }$$

Lean4

theorem isTightMeasureSet_of_tendsto_measure_norm_gt [ProperSpace E]
    (h : Tendsto (fun r : ℝ ↦ ⨆ μ ∈ S, μ {x | r < ‖x‖}) atTop (𝓝 0)) : IsTightMeasureSet S :=
  by
  refine isTightMeasureSet_of_tendsto_measure_compl_closedBall (x := 0) ?_
  convert h using 6 with r
  ext
  simp

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