Theorems · Definition

EquivLike.toEquiv

{α : Sort u} → {β : Sort v} → {F : Sort u_1} → [EquivLike F α β] → F → α ≃ β

Turn an element of a type F satisfying EquivLike F α β into an actual Equiv. This is declared as the default coercion from F to α ≃ β.

Defined in

Mathlib.Logic.Equiv.Defs

Cited by

125 results in Mathlib

Foundations

Depth 10 from the axioms, rests on 53 definitions · uses Quot.sound

Assumes

EquivLike