Skip to content

Instantly share code, notes, and snippets.

@maoe

maoe/Existentials.v

Created May 29, 2011 17:54
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save maoe/997989 to your computer and use it in GitHub Desktop.
Save maoe/997989 to your computer and use it in GitHub Desktop.
Download ZIP
(∃x.P(x)) → Q ⇔ ∀x.(P(x) → Q)の証明
Raw
Existentials.v
Lemma L0 : forall (A : Type) (P : A -> Prop) (Q : Prop),
((exists x, P x) -> Q) -> (forall x, P x -> Q).
Proof.
intros.
apply H.
exists x.
apply H0.
Qed.
Lemma L1 : forall (A : Type) (P : A -> Prop) (Q : Prop),
(forall x, P x -> Q) -> ((exists x, P x) -> Q).
Proof.
intros.
case H0.
apply H.
Qed.
Theorem L2 : forall (A : Type) (P : A -> Prop) (Q : Prop),
((exists x, P x) -> Q) <-> (forall x, P x -> Q).
Proof.
intros.
unfold iff.
split.
apply L0.
apply L1.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment