English
For a simple function f, f has finite μ-measurable support if and only if for every nonzero value y, the μ-measure of the set where f takes the value y is finite.
Русский
Для простой функции f единственно верно: f имеет конечную опору по мере μ тогда и только если для каждого ненулевого значения y множество f⁻¹({y}) имеет конечную меру μ.
LaTeX
$$$\mathrm{FinMeasSupp}(f,\mu) \iff \forall y\, (y \neq 0 \Rightarrow \mu(f^{-1}({y})) < \infty)$$$
Lean4
theorem finMeasSupp_iff : f.FinMeasSupp μ ↔ ∀ y, y ≠ 0 → μ (f ⁻¹' { y }) < ∞ := by
classical
constructor
· refine fun h y hy => lt_of_le_of_lt (measure_mono ?_) h
exact fun x hx (H : f x = 0) => hy <| H ▸ Eq.symm hx
· intro H
rw [finMeasSupp_iff_support, support_eq]
exact measure_biUnion_lt_top (finite_toSet _) fun y hy ↦ H y (mem_filter.1 hy).2
