lintegral_eq_zero_iff — Mathlib

English

For f ∈ α →ₘ[μ] ℝ≥0∞, lintegral f = 0 if and only if f = 0.

Русский

Для f ∈ α →ₘ[μ] ℝ≥0∞, линтеграл f равен нулю тогда и только тогда, когда f = 0.

LaTeX

$$lintegral_eq_zero_iff {f : α →ₘ[μ] ℝ≥0∞} : lintegral f = 0 ↔ f = 0$$

Lean4

@[simp]
theorem lintegral_eq_zero_iff {f : α →ₘ[μ] ℝ≥0∞} : lintegral f = 0 ↔ f = 0 :=
  induction_on f fun _f hf => (lintegral_eq_zero_iff' hf.aemeasurable).trans mk_eq_mk.symm

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