mathlib documentation

lean_problem_sheets / 2020.functions.two_sided_inverse

Two-sided inverses #

We define two-sided inverses, and prove that a function is a bijection if and only if it has a two-sided inverse.

source
structure two_sided_inverse {X Y : Type} (f : X → Y) :
Type
  • g : Y → X
  • hX : ∀ (x : X), self.g (f x) = x
  • hY : ∀ (y : Y), f (self.g y) = y