finMeasSupp_iff_support — Mathlib

English

Let f be a simple function with respect to μ. Then f has finite μ-measurable support if and only if the μ-measure of its support is finite.

Русский

Пусть f — простая функция относительно μ. Тогда фукция имеет конечную опору по мере μ тогда и только если μ(опора(f)) конечна.

LaTeX

$$$\mathrm{FinMeasSupp}(f,\mu) \iff \mu(\operatorname{supp}(f)) < \infty$$$

Lean4

theorem finMeasSupp_iff_support : f.FinMeasSupp μ ↔ μ (support f) < ∞ :=
  Iff.rfl

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