measure_ne_zero_iff_nonempty_of_isMulLeftInvariant

English

For a regular left-invariant measure μ with μ ≠ 0, for every open set s, μ(s) ≠ 0 iff s is nonempty.

Русский

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

LaTeX

$$$\mu \neq 0 \quad \Rightarrow \quad \forall s\, (\text{IsOpen}(s)) \Rightarrow (\mu(s) \neq 0 \iff s.Nonempty)$$$

Lean4

@[to_additive]
theorem measure_ne_zero_iff_nonempty_of_isMulLeftInvariant [Regular μ] (hμ : μ ≠ 0) {s : Set G} (hs : IsOpen s) :
    μ s ≠ 0 ↔ s.Nonempty := by simpa [null_iff_of_isMulLeftInvariant (μ := μ) hs, hμ] using nonempty_iff_ne_empty.symm

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