isTightMeasureSet_of_inner_tendsto

English

If S consists of finite measures inner regular with respect to closed sets, then S is tight.

Русский

Если S состоит из конечных мер, которые внутренне регулярны по отношению к замкнутым множествам, то S плотна.

LaTeX

$$isTightMeasureSet_singleton_of_innerRegularWRT$$

Lean4

theorem isTightMeasureSet_of_inner_tendsto
    (h : ∀ y, Tendsto (fun r : ℝ ↦ ⨆ μ ∈ S, μ {x | r < ‖⟪y, x⟫_𝕜‖}) atTop (𝓝 0)) : IsTightMeasureSet S :=
  isTightMeasureSet_of_forall_basis_tendsto (stdOrthonormalBasis 𝕜 E) fun i ↦ h (stdOrthonormalBasis 𝕜 E i)

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