equiv_of_isEmpty

Mathlib.SetTheory.ZFC.PSet

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

English

If x,y are PSet with empty types, then x ≃ y.

Русский

Если x,y — PSet и их типы пустые, то x ≃ y.

LaTeX

$$∀ (x y : PSet), [IsEmpty x.Type] [IsEmpty y.Type] → Equiv x y$$

Lean4

protected theorem equiv_of_isEmpty (x y : PSet) [IsEmpty x.Type] [IsEmpty y.Type] : Equiv x y :=
  equiv_iff.2 <| by simp

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

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

Разделы

Аффилиация

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