exists_measure_inter_spanningSets_pos

English

There exists n such that μ(s ∩ spanningSets(μ, n)) > 0 iff μ(s) > 0.

Русский

Существуют n такие, что μ(s ∩ spanningSets(μ, n)) > 0 тогда и только тогда μ(s) > 0.

LaTeX

$$(∃ n, 0 < μ(s ∩ spanningSets(μ, n))) ⇔ 0 < μ(s)$$

Lean4

/-- A set in a σ-finite space has positive measure if and only if its intersection with
some member of the countable family of finite measure spanning sets has positive measure. -/
theorem exists_measure_inter_spanningSets_pos [MeasurableSpace α] {μ : Measure α} [SigmaFinite μ] (s : Set α) :
    (∃ n, 0 < μ (s ∩ spanningSets μ n)) ↔ 0 < μ s :=
  by
  rw [← not_iff_not]
  simp only [not_exists, not_lt, nonpos_iff_eq_zero]
  exact forall_measure_inter_spanningSets_eq_zero s

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