mapEquiv — Mathlib

English

There is a transported equivalence for a bifunctor F given two equivalences h and h'.

Русский

Существуют переносимые эквивалентности для бифункторной структуры F, заданной двумя эквивалентностями h и h'.

LaTeX

$$$ (\\text{mapEquiv } F\; h\; h') : F\\ α\\ α' \\simeq F\\ β\\ β' $ with toFun = \\text{bimap } h\ h' and invFun = \\text{bimap } h^{-1}\\ h'^{-1}$$$

Lean4

/-- Apply a bifunctor to a pair of `Equiv`s. -/
def mapEquiv (h : α ≃ β) (h' : α' ≃ β') : F α α' ≃ F β β'
    where
  toFun := bimap h h'
  invFun := bimap h.symm h'.symm
  left_inv x := by simp [bimap_bimap, id_bimap]
  right_inv x := by simp [bimap_bimap, id_bimap]

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