measure_preimage_eq_zero_iff_of_countable

English

For s countable, μ(f^{-1} s) = 0 iff ∀ x ∈ s, μ(f^{-1} {x}) = 0.

Русский

Для счетного множества s верно: μ(f^{-1}(s)) = 0 тогда и только если для каждого x ∈ s выполняется μ(f^{-1}({x})) = 0.

LaTeX

$$$$ \\mu\\left(f^{-1}(s)\\right) = 0 \\iff \\forall x \\in s, \\mu\\left(f^{-1}\\{x\\}\\right) = 0. $$$$

Lean4

theorem measure_preimage_eq_zero_iff_of_countable {s : Set β} {f : α → β} (hs : s.Countable) :
    μ (f ⁻¹' s) = 0 ↔ ∀ x ∈ s, μ (f ⁻¹' { x }) = 0 := by rw [← biUnion_preimage_singleton, measure_biUnion_null_iff hs]

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