copy

Mathlib.Order.RelIso.Basic

URI: https://scilib.ai/kg/mathlib#RelIso.copy

Lean4

/-- Copy of a `RelIso` with a new `toFun` and `invFun` equal to the old ones.
Useful to fix definitional equalities. -/
def copy (e : r ≃r s) (f : α → β) (g : β → α) (hf : f = e) (hg : g = e.symm) : r ≃r s
    where
  toFun := f
  invFun := g
  left_inv _ := by simp [hf, hg]
  right_inv _ := by simp [hf, hg]
  map_rel_iff' := by simp [hf, e.map_rel_iff]

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

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

Разделы

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

Аффилиация

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