sumEmpty_apply_inl

Mathlib.Logic.Equiv.Sum

URI: https://scilib.ai/kg/mathlib#Equiv.sumEmpty_apply_inl

English

The sumEmpty equivalence sends inl a to a.

Русский

Эквивалентность sumEmpty отправляет inl a в a.

LaTeX

$$$$\mathrm{sumEmpty}(\alpha, \beta)(\mathrm{inl}(a)) = a.$$$$

Lean4

@[simp]
theorem sumEmpty_apply_inl {α β} [IsEmpty β] (a : α) : sumEmpty α β (Sum.inl a) = a :=
  rfl

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

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

Разделы

Аффилиация

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