measure_eq_zero_iff_eq_empty_of_smulInvariant

English

Under SMulInvariantMeasure and minimal action, μ(U) = 0 implies U = ∅ for open U.

Русский

При SMulInvariantMeasure и минимальном действии μ(U) = 0 тогда и только если U = ∅ для открытого U.

LaTeX

$$$μ(U) = 0 \\iff U = \\emptyset$$$

Lean4

@[to_additive]
theorem measure_eq_zero_iff_eq_empty_of_smulInvariant (hμ : μ ≠ 0) (hU : IsOpen U) : μ U = 0 ↔ U = ∅ := by
  rw [← not_iff_not, ← Ne, ← pos_iff_ne_zero, measure_pos_iff_nonempty_of_smulInvariant G hμ hU, nonempty_iff_ne_empty]

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