∃a∀b[P(a, b)] → ∀b∃a[P(a, b)] Lemma exists_forall : forall (A:Type)(P: A -> A -> Prop), (exists a:A, forall b:A, P a b) -> (forall b:A, exists a:A, P a b). Proof. intros A P H1 a. elim H1. intros x H2. exists x. apply H2. Qed.
引用をストックしました
引用するにはまずログインしてください
引用をストックできませんでした。再度お試しください
限定公開記事のため引用できません。