Documentation

Init.Grind.Injective

source
noncomputable def Lean.Grind.leftInv {α : Sort u} {β : Sort v} (f : α → β) (hf : Function.Injective f) [Nonempty α] :
β → α
Instances For
    source
    theorem Lean.Grind.leftInv_eq {α : Sort u} {β : Sort v} (f : α → β) (hf : Function.Injective f) [Nonempty α] (a : α) :
    f⁻¹ (f a) = a
    source
    def Lean.Grind.leftInvUnexpander :
    PrettyPrinter.Unexpander
    Instances For