instEmptyCollection — Mathlib

English

There exists an empty collection in the subtype of measurable sets: the element consisting of the empty set with the corresponding measurability proof.

Русский

Существует пустая коллекция элементов подтипа измеримых множеств: элемент, состоящий из пустого множества и соответствующего доказательства измеримости.

LaTeX

$$$$\\text{There exists } s = (\\emptyset, \\text{MeasurableSet.empty}) \\in \\text{Subtype}(\\text{MeasurableSet}) .$$$$

Lean4

instance instEmptyCollection : EmptyCollection (Subtype (MeasurableSet : Set α → Prop)) :=
  ⟨⟨∅, MeasurableSet.empty⟩⟩

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