Theorems · Theorem

Equiv.mk.congr_simp

∀ {α : Sort u_1} {β : Sort u_2} (toFun toFun_1 : α → β) (e_toFun : toFun = toFun_1) (invFun invFun_1 : β → α)
  (e_invFun : invFun = invFun_1) (left_inv : Function.LeftInverse invFun toFun)
  (right_inv : Function.RightInverse invFun toFun),
  { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv } =
    { toFun := toFun_1, invFun := invFun_1, left_inv := ⋯, right_inv := ⋯ }

Defined in

Mathlib.Logic.Equiv.Defs

Cited by

54 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms