nonempty_measurable_superset — Mathlib

English

For any set s ⊆ α, there exists a measurable superset t of s.

Русский

Для любого множества s ⊆ α существует измеримое надмножество t, содержащее s.

LaTeX

$$$\exists t \; (s \subseteq t \land \mathrm{MeasurableSet}(t))$$$

Lean4

/-- Every set has a measurable superset. Declare this as local instance as needed. -/
theorem nonempty_measurable_superset (s : Set α) : Nonempty { t // s ⊆ t ∧ MeasurableSet t } :=
  ⟨⟨univ, subset_univ s, MeasurableSet.univ⟩⟩

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