instIsEmptyInvTyTrue

Mathlib.SetTheory.Game.Basic

URI: https://scilib.ai/kg/mathlib#SetTheory.PGame.instIsEmptyInvTyTrue

English

If both left and right types are empty, then InvTy l r true is empty.

Русский

Если слева и справа оба типа пусты, InvTy l r true пуст.

LaTeX

$$$\text{IsEmpty}(\text{InvTy}(l,r,\text{Bool.true}))$$$

Lean4

instance (l r : Type u) [IsEmpty l] [IsEmpty r] : IsEmpty (InvTy l r true) :=
  ⟨by rintro (_ | _ | _ | a | a) <;> exact isEmptyElim a⟩

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

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

Разделы

Аффилиация

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