nonempty — Mathlib

English

If a family 𝒜 is measure-dense, then it contains at least one set.

Русский

Если 𝒜 плотна по мере, она содержит хотя бы одно множество.

LaTeX

$$$ (\\text{h𝒜: } μ.\\text{MeasureDense } 𝒜) \\Rightarrow 𝒜\\text{.Nonempty} $$$

Lean4

theorem nonempty (h𝒜 : μ.MeasureDense 𝒜) : 𝒜.Nonempty :=
  by
  rcases h𝒜.approx ∅ MeasurableSet.empty (by simp) 1 (by simp) with ⟨t, ht, -⟩
  exact ⟨t, ht⟩

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