Step
*
of Lemma
prob2.4
∀[U:Type]. ∀[P,Q:U ⟶ ℙ]. ((∃x:U. ((P x) ∧ (Q x)))
⇒ ((∃x:U. (P x)) ∧ (∃x:U. (Q x))))
BY
{ (Auto⋅ THEN ExRepD THEN Auto) }
Latex:
Latex:
\mforall{}[U:Type]. \mforall{}[P,Q:U {}\mrightarrow{} \mBbbP{}]. ((\mexists{}x:U. ((P x) \mwedge{} (Q x))) {}\mRightarrow{} ((\mexists{}x:U. (P x)) \mwedge{} (\mexists{}x:U. (Q x))))
By
Latex:
(Auto\mcdot{} THEN ExRepD THEN Auto)
Home
Index