rangeInl_apply_inl

Mathlib.Logic.Equiv.Set

URI: https://scilib.ai/kg/mathlib#Equiv.Set.rangeInl_apply_inl

English

(rangeInl α β)(⟨inl x, mem_range_self⟩) = x.

Русский

Применение rangeInl к ⟨inl x, mem_range_self⟩ даёт x.

LaTeX

$$$(\\mathrm{rangeInl}\\\\(\\alpha,\\\\\\beta))\\\\(\\\\langle \\\\mathrm{inl} x, \\\\mathrm{mem\\_range\\_self} \\\\rangle) = x$$$

Lean4

@[simp]
theorem rangeInl_apply_inl {α : Type*} (β : Type*) (x : α) : (rangeInl α β) ⟨.inl x, mem_range_self _⟩ = x :=
  rfl

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

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

Разделы

Аффилиация

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