measure_support_lt_top — Mathlib

English

If for every nonzero y the preimage μ(f^{-1}({y})) is finite, then μ(support f) is finite.

Русский

Если для каждого ненулевого y множества f^{-1}({y}) имеет конечную меру, то μ(support f) конечна.

LaTeX

$$$\\forall y, y \\neq 0 \\implies μ(f^{-1}({y})) < \\infty \\;\; \\Rightarrow\\; μ(\\operatorname{support} f) < \\infty$$$

Lean4

theorem measure_support_lt_top (f : α →ₛ β) (hf : ∀ y, y ≠ 0 → μ (f ⁻¹' { y }) < ∞) : μ (support f) < ∞ := by
  classical
  rw [support_eq]
  refine (measure_biUnion_finset_le _ _).trans_lt (ENNReal.sum_lt_top.mpr fun y hy => ?_)
  rw [Finset.mem_filter] at hy
  exact hf y hy.2

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