measure_pos_iff_nonempty_of_smulInvariant

English

For μ ≠ 0 and open U, μ(U) > 0 if and only if U is nonempty.

Русский

Для μ ≠ 0 и открытого U выполняется μ(U) > 0 тогда и только если U непусто.

LaTeX

$$$0 < μ(U) \\iff U \\neq \\emptyset$$$

Lean4

@[to_additive]
theorem measure_pos_iff_nonempty_of_smulInvariant (hμ : μ ≠ 0) (hU : IsOpen U) : 0 < μ U ↔ U.Nonempty :=
  ⟨fun h => nonempty_of_measure_ne_zero h.ne', measure_isOpen_pos_of_smulInvariant_of_ne_zero G hμ hU⟩

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