equiv_empty

Mathlib.SetTheory.ZFC.PSet

URI: https://scilib.ai/kg/mathlib#PSet.equiv_empty

English

If a pre-set x has an empty type, then x is equivalent to the empty pre-set.

Русский

Если тип пред-множества x пуст, то x эквивалентно пустому пред-множу.

LaTeX

$$$$ \forall x\,[ \mathrm{IsEmpty}(x.\mathrm{Type}) \Rightarrow x \equiv \emptyset ] $$$$

Lean4

protected theorem equiv_empty (x : PSet) [IsEmpty x.Type] : Equiv x ∅ :=
  PSet.equiv_of_isEmpty x _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru