self_iff — Mathlib

English

A measure μ is mutually singular with itself if and only if μ = 0.

Русский

Мера μ взаимно неразделима с самой собой тогда и только тогда, когда μ = 0.

LaTeX

$$$\\mu \\perp_m \\mu \\quad\\Leftrightarrow\\quad \\mu = 0$$$

Lean4

@[simp]
theorem self_iff (μ : Measure α) : μ ⟂ₘ μ ↔ μ = 0 :=
  by
  refine ⟨?_, fun h ↦ by (rw [h]; exact zero_left)⟩
  rintro ⟨s, hs, hμs, hμs_compl⟩
  suffices μ Set.univ = 0 by rwa [measure_univ_eq_zero] at this
  rw [← Set.union_compl_self s, measure_union disjoint_compl_right hs.compl, hμs, hμs_compl, add_zero]

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