Theorems · Inductive type

EquivLike

Sort u_1 → outParam (Sort u_2) → outParam (Sort u_3) → Sort (max (max (max 1 u_1) u_2) u_3)

The class EquivLike E α β expresses that terms of type E have an injective coercion to bijections between α and β. Note that this does not directly extend FunLike, nor take FunLike as a parameter, so we can state coe_injective' in a nicer way. This typeclass is used in the definition of the isomorphism (or equivalence) typeclasses, such as ZeroEquivClass, MulEquivClass, MonoidEquivClass, ....

Defined in

Mathlib.Data.FunLike.Equiv

Cited by

165 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms