rangeInr_apply_inr

Mathlib.Logic.Equiv.Set

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

English

(rangeInr α β)(⟨inr x, _⟩) = x.

Русский

Применение rangeInr к ⟨inr x, ⟩ даёт x.

LaTeX

$$$(\\mathrm{rangeInr}\\\\(α,\\\\β))\\\\(\\\\langle \\\\mathrm{inr} x, \\\\mathrm{mem\\_range\\_self} \\\\rangle) = x$$$

Lean4

@[simp]
theorem rangeInr_apply_inr (α : Type*) {β : Type*} (x : β) : (rangeInr α β) ⟨.inr x, mem_range_self _⟩ = x :=
  rfl

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

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

Разделы

Аффилиация

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