Skip to content

Instantly share code, notes, and snippets.

@leodemoura

leodemoura/inj2.lean

Last active December 26, 2019 11:35
Show Gist options
  • Star 2 You must be signed in to star a gist
  • Fork 1 You must be signed in to fork a gist
  • Save leodemoura/0c88341bb585bf9a72e6 to your computer and use it in GitHub Desktop.
Save leodemoura/0c88341bb585bf9a72e6 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
inj2.lean
open eq
inductive I (F : Type₁ → Prop) : Type₁ :=
mk : I F
axiom InjI : ∀ {x y}, I x = I y → x = y
definition P (x : Type₁) : Prop := ∃ a, I a = x ∧ (a x → false).
definition p := I P
lemma false_of_Pp (H : P p) : false :=
obtain a Ha0 Ha1, from H,
subst (InjI Ha0) Ha1 H
lemma contradiction : false :=
have Pp : P p, from exists.intro P (and.intro rfl false_of_Pp),
false_of_Pp Pp
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment