fromTypes_nil

Mathlib.Logic.Function.FromTypes

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

English

FromTypes ![] τ = τ by zero case.

Русский

FromTypes ![] τ равно τ по базовому случаю нуля, аналогично FromTypes_zero.

LaTeX

$$$FromTypes ![]\,\tau = \tau$$$

Lean4

theorem fromTypes_nil (τ : Type u) : FromTypes ![] τ = τ :=
  fromTypes_zero ![] τ

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

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

Разделы

Аффилиация

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