meas_preimage_singleton_ne_zero — Mathlib

English

If f has finite μ-measurable support, then for any nonzero y, the preimage of {y} under f has finite μ-measure.

Русский

Если у f конечная по μ опора, то для любого ненулевого y множество f⁻¹({y}) имеет конечную меру μ.

LaTeX

$$$\mathrm{FinMeasSupp}(f,\mu) \Rightarrow \forall y\,(y \neq 0 \Rightarrow \mu(f^{-1}({y})) < \infty)$$$

Lean4

theorem meas_preimage_singleton_ne_zero (h : f.FinMeasSupp μ) {y : β} (hy : y ≠ 0) : μ (f ⁻¹' { y }) < ∞ :=
  finMeasSupp_iff.1 h y hy

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