measure_pos_iff_nonempty_of_isMulLeftInvariant

English

For a regular left-invariant μ with μ ≠ 0 and s open, 0 < μ(s) iff s is nonempty.

Русский

Для регулярной лево-инвариантной μ с μ ≠ 0 и открытым s верно: 0 < μ(s) ↔ s ≠ ∅.

LaTeX

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

Lean4

@[to_additive]
theorem measure_pos_iff_nonempty_of_isMulLeftInvariant [Regular μ] (h3μ : μ ≠ 0) {s : Set G} (hs : IsOpen s) :
    0 < μ s ↔ s.Nonempty :=
  pos_iff_ne_zero.trans <| measure_ne_zero_iff_nonempty_of_isMulLeftInvariant h3μ hs

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