single

Mathlib.Data.PEquiv

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

Lean4

/-- Create a `PEquiv` which sends `a` to `b` and `b` to `a`, but is otherwise `none`. -/
def single (a : α) (b : β) : α ≃. β where
  toFun x := if x = a then some b else none
  invFun x := if x = b then some a else none
  inv x
    y := by
    split_ifs with h1 h2
    · simp [*]
    · simp only [some.injEq, iff_false] at *
      exact Ne.symm h2
    · simp only [some.injEq, false_iff] at *
      exact Ne.symm h1
    · simp

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

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

Разделы

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

Аффилиация

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