Skip to content

Instantly share code, notes, and snippets.

@luxbock luxbock/halp.lean
Created Sep 10, 2018

Embed
What would you like to do?
open classical
variables (α : Type) (p q : α → Prop)
variable r : Prop
variable a : α
example : (∃ x, p x → r) ↔ (∀ x, p x) → r :=
iff.intro
(assume ⟨a, pair⟩,
assume h : ∀ x, p x,
show r, from pair $ h a)
(assume h : (∀ (x : α), p x) → r,
suffices pair : p a → r, from ⟨a, pair⟩,
have hr : r, from h (λ y, _),
/-
context:
α : Type,
p : α → Prop,
r : Prop,
a : α,
h : (∀ (x : α), p x) → r,
y : α
⊢ p y
-/
(λ hpa, hr))
example : (∃ x, r → p x) ↔ (r → ∃ x, p x) :=
iff.intro
(assume ⟨ha, ripa⟩,
assume hr,
show ∃ x, p x, from ⟨ha, ripa hr⟩)
(assume h : r → (∃ (x : α), p x),
suffices ripa : r → p a, from ⟨a, ripa⟩,
assume hr,
have x : (∃ x, p x), from h hr,
exists.elim x
(assume ha,
assume hpa,
_))
/-
context:
α : Type,
p : α → Prop,
r : Prop,
a : α,
h : r → (∃ (x : α), p x),
hr : r,
x : ∃ (x : α), p x,
ha : α,
hpa : p ha
⊢ p a
-/
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.