Skip to content

Instantly share code, notes, and snippets.

@fehrenbach

fehrenbach/ideminvoid.lean

Last active November 18, 2015 10:47
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save fehrenbach/29d5c1befe00d6eb697f to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save fehrenbach/29d5c1befe00d6eb697f to your computer and use it in GitHub Desktop.
Download ZIP
Raw
ideminvoid.lean
open function
lemma ideminvoid (A : Type)
(f : A -> A)
(f_idem : forall x, f (f x) = f x)
(f_invo : forall x, f (f x) = x)
: forall x, f x = id x :=
take x, calc f x = f (f x) : f_idem
... = x : f_invo
... = id x : rfl
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment