comp_null — Mathlib

English

If (η ∘ κ) a s ≠ ∞, then for κ-a.e. b (with respect to κ a), η b s < ∞.

Русский

Если (η ∘ κ) a s не бесконечно, то для почти всех b по мере κ a выполнено, что η b s < ∞.

LaTeX

$$$(\\eta \\circ_k \\kappa)(a,s) \\neq \\infty \\Rightarrow \\forall^{\\mathrm{ae}} b \\partial (\\kappa a),\\; \\eta(b,s) < \\infty.$$$

Lean4

theorem comp_null (a : α) (hs : MeasurableSet s) : (η ∘ₖ κ) a s = 0 ↔ (fun y ↦ η y s) =ᵐ[κ a] 0 := by
  rw [comp_apply' _ _ _ hs, lintegral_eq_zero_iff (η.measurable_coe hs)]

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