exists_isCompact_not_null — Mathlib

English

For a regular measure μ, μ ≠ 0 if and only if there exists a compact set K with μ(K) ≠ 0.

Русский

Для регулярной меры μ ≠ 0 тогда и только тогда существует компактное множество K такое, что μ(K) ≠ 0.

LaTeX

$$$\\mu \\neq 0 \\quad\\text{iff}\\quad \\exists K, \\operatorname{IsCompact}(K) \\wedge \\mu(K) \\neq 0.$$$

Lean4

theorem exists_isCompact_not_null [Regular μ] : (∃ K, IsCompact K ∧ μ K ≠ 0) ↔ μ ≠ 0 := by
  simp_rw [Ne, ← measure_univ_eq_zero, isOpen_univ.measure_eq_iSup_isCompact, ENNReal.iSup_eq_zero, not_forall,
    exists_prop, subset_univ, true_and]

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