measure_inter_conull — Mathlib

English

Let μ be a measure on α. If t is co-null (μ(t^c) = 0), then for any s, μ(s ∩ t) = μ(s).

Русский

Пусть μ — мера на α. Пусть t является коннулльным, т.е. μ(t^c) = 0. Тогда для любого множества s верно μ(s ∩ t) = μ(s).

LaTeX

$$$ \mu(t^{c}) = 0 \;\Rightarrow\; \mu(s \cap t) = \mu(s)$$$

Lean4

theorem measure_inter_conull (ht : μ tᶜ = 0) : μ (s ∩ t) = μ s := by rw [← diff_compl, measure_diff_null ht]

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