instIsEmpty

Mathlib.Data.W.Basic

URI: https://scilib.ai/kg/mathlib#WType.instIsEmpty

English

If α is an empty type, then WType β is also empty.

Русский

Если α пустой тип, то и WType β пустой.

LaTeX

$$$\text{IsEmpty}(\alpha) \Rightarrow \text{IsEmpty}(WType(\beta)).$$$

Lean4

instance [hα : IsEmpty α] : IsEmpty (WType β) :=
  ⟨fun w => WType.recOn w (IsEmpty.elim hα)⟩

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

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

Разделы

Аффилиация

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