optionEquivSumPUnit_some

Mathlib.Logic.Equiv.Option

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

English

The image of some a under optionEquivSumPUnit α is inl a.

Русский

Образ some a под optionEquivSumPUnit α лежит в inl a.

LaTeX

$$$\mathrm{optionEquivSumPUnit}\;\alpha\;(\mathrm{some}\; a) = \mathrm{Sum}.\mathrm{inl} \; a$$$

Lean4

@[simp]
theorem optionEquivSumPUnit_some {α} (a) : optionEquivSumPUnit α (some a) = Sum.inl a :=
  rfl

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

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

Разделы

Аффилиация

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