mathlib documentation

Equations

• canonical α = {to_fun := λ (P : α → Prop), {x : α | P x}, inv_fun := λ (X : set α) (a : α), a ∈ X, left_inv := _, right_inv := _}