我试图证明以下引理:
lemma myLemma6: "(∀x. A(x) ∧ B(x))= ((∀x. A(x)) ∧ (∀x. B(x)))"
我试图从消除 forall 量词开始,所以这就是我尝试过的:
lemma myLemma6: "(∀x. A(x) ∧ B(x))= ((∀x. A(x)) ∧ (∀x. B(x)))"
apply(rule iffI)
apply ( erule_tac x="x" in allE)
apply (rule allE)
(*goal now: get rid of conj on both sides and the quantifiers on right*)
apply (erule conjE) (*isn't conjE supposed to be used with elim/erule?*)
apply (rule allI)
apply (assumption)
apply ( rule conjI) (*at this point, the following starts to make no sense... *)
apply (rule conjE) (*should be erule?*)
apply ( rule conjI)
apply ( rule conjI)
...
最后我刚刚开始根据之前申请的结果采取行动,但对我来说似乎是错误的,可能是因为一开始有一些错误......有人可以向我解释我的错误以及如何正确完成这个证明?
提前致谢