single

Mathlib.Logic.Equiv.PartialEquiv

URI: https://scilib.ai/kg/mathlib#PartialEquiv.single

Lean4

/-- `Function.const` as a `PartialEquiv`.
It consists of two constant maps in opposite directions. -/
@[simps]
def single (a : α) (b : β) : PartialEquiv α β
    where
  toFun := Function.const α b
  invFun := Function.const β a
  source := { a }
  target := { b }
  map_source' _ _ := rfl
  map_target' _ _ := rfl
  left_inv' a' ha' := by rw [eq_of_mem_singleton ha', const_apply]
  right_inv' b' hb' := by rw [eq_of_mem_singleton hb', const_apply]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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