null_iff_of_isMulLeftInvariant — Mathlib

English

For a regular left-invariant measure μ, and an open set s, μ(s) = 0 iff s = ∅ or μ = 0.

Русский

Для регулярной лево-инвариантной меры μ и открытого множества s выполнено: μ(s) = 0 тогда и только тогда, когда s = ∅ или μ = 0.

LaTeX

$$$\text{IsOpen}(s) \Rightarrow \mu(s) = 0 \iff s = \varnothing \lor \mu = 0$$$

Lean4

@[to_additive]
theorem null_iff_of_isMulLeftInvariant [Regular μ] {s : Set G} (hs : IsOpen s) : μ s = 0 ↔ s = ∅ ∨ μ = 0 :=
  by
  rcases eq_zero_or_neZero μ with rfl | hμ
  · simp
  · simp only [or_false, hs.measure_eq_zero_iff μ, NeZero.ne μ]

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