empty_def — Mathlib

English

The empty pre-set is the object built from the empty type with the empty-membership constructor.

Русский

Пустое пред-множество есть объект, построенный из пустого типа с помощью функции пустой принадлежности.

LaTeX

$$$$ \emptyset_{\mathrm{PSet}} = \langle \emptyset, \mathrm{PEmpty.elim} \rangle $$$$

Lean4

theorem empty_def : (∅ : PSet) = ⟨_, PEmpty.elim⟩ := by simp [EmptyCollection.emptyCollection, PSet.empty]

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