Theorems · Theorem

EquivLike.inv_apply_apply

∀ {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [inst : EquivLike E α β] (e : E) (a : α), EquivLike.inv e (e a) = a

This lemma is only supposed to be used in the generic context, when working with instances of classes extending EquivLike. For concrete isomorphism types such as Equiv, you should use Equiv.symm_apply_apply or its equivalent. TODO: define a generic form of Equiv.symm.

Defined in

Mathlib.Data.FunLike.Equiv

Cited by

3 results in Mathlib

Foundations

Depth 9 from the axioms · uses Quot.sound

Assumes

EquivLike