finiteAt_inner — Mathlib

English

If l is an FTC-filter around a, then for any locally finite measure μ, μ is finite on the inner filter l'.

Русский

Пусть l — фильтр вокруг a, тогда для любой локально ограниченной меры μ справедливо, что μ конечна на внутреннем фильтре l'.

LaTeX

$$$\\mu.FiniteAtFilter(l')$$$

Lean4

theorem finiteAt_inner {a : ℝ} (l : Filter ℝ) {l'} [h : FTCFilter a l l'] {μ : Measure ℝ} [IsLocallyFiniteMeasure μ] :
    μ.FiniteAtFilter l' :=
  (μ.finiteAt_nhds a).filter_mono h.le_nhds

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