nonempty' — Mathlib

English

The collection of measurable sets is measure-dense.

Русский

Собрание измеримых множеств является measure-dense.

LaTeX

$$$ \\mu.MeasureDense \\{s \\mid \\mathrm{MeasurableSet}(s)\\} $$$

Lean4

theorem nonempty' (h𝒜 : μ.MeasureDense 𝒜) : {s | s ∈ 𝒜 ∧ μ s ≠ ∞}.Nonempty :=
  by
  rcases h𝒜.approx ∅ MeasurableSet.empty (by simp) 1 (by simp) with ⟨t, ht, hμt⟩
  refine ⟨t, ht, ?_⟩
  convert ne_top_of_lt hμt
  rw [← bot_eq_empty, bot_symmDiff]

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