exists_mem_of_measure_ne_zero_of_ae

English

If μ(s) ≠ 0 and p holds almost everywhere on s, then there exists x ∈ s with p(x).

Русский

Если μ(s) ≠ 0 и p выполняется почти всюду на s, то существует x ∈ s такое что p(x).

LaTeX

$$$μ\,s \neq 0 \implies (∀^{ae} x ∂μ.restrict s, p x) \Rightarrow ∃ x, x ∈ s ∧ p x$$$

Lean4

theorem exists_mem_of_measure_ne_zero_of_ae (hs : μ s ≠ 0) {p : α → Prop} (hp : ∀ᵐ x ∂μ.restrict s, p x) :
    ∃ x, x ∈ s ∧ p x := by
  rw [← μ.restrict_apply_self, ← frequently_ae_mem_iff] at hs
  exact (hs.and_eventually hp).exists

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