instFunLikeOption

Mathlib.Data.PEquiv

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

Lean4

instance : FunLike (α ≃. β) α (Option β) :=
  { coe := toFun
    coe_injective' := by
      rintro ⟨f₁, f₂, hf⟩ ⟨g₁, g₂, hg⟩ (rfl : f₁ = g₁)
      congr with y x
      simp only [hf, hg] }

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

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

Разделы

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

Аффилиация

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