fromTypes_zero

Mathlib.Logic.Function.FromTypes

URI: https://scilib.ai/kg/mathlib#Function.fromTypes_zero

English

FromTypes p τ equals τ when p is the empty index Fin 0 → Type.

Русский

FromTypes p τ равно τ, если p имеет пустой индекс Fin 0 → Type.

LaTeX

$$$FromTypes p\,\tau = \tau$$$

Lean4

theorem fromTypes_zero (p : Fin 0 → Type u) (τ : Type u) : FromTypes p τ = τ :=
  rfl

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

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

Разделы

Аффилиация

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