Step
*
of Lemma
decidable-predicate-and
∀[T,S:Type]. ∀[A:T ⟶ ℙ]. ∀[B:S ⟶ ℙ].
((∃t:T. (A t))
⇒ (∃s:S. (B s))
⇒ (∀p:T × S. Dec(predicate-and(A;B) p)
⇐⇒ (∀x:T. Dec(A x)) ∧ (∀y:S. Dec(B y))))
BY
{ (Auto THEN ExRepD) }
1
1. [T] : Type
2. [S] : Type
3. [A] : T ⟶ ℙ
4. [B] : S ⟶ ℙ
5. t : T@i
6. A t@i
7. s : S@i
8. B s@i
9. ∀p:T × S. Dec(predicate-and(A;B) p)@i
10. x : T@i
⊢ Dec(A x)
2
1. [T] : Type
2. [S] : Type
3. [A] : T ⟶ ℙ
4. [B] : S ⟶ ℙ
5. t : T@i
6. A t@i
7. s : S@i
8. B s@i
9. ∀p:T × S. Dec(predicate-and(A;B) p)@i
10. y : S@i
⊢ Dec(B y)
3
1. [T] : Type
2. [S] : Type
3. [A] : T ⟶ ℙ
4. [B] : S ⟶ ℙ
5. t : T@i
6. A t@i
7. s : S@i
8. B s@i
9. ∀x:T. Dec(A x)@i
10. ∀y:S. Dec(B y)@i
11. p : T × S@i
⊢ Dec(predicate-and(A;B) p)
Latex:
Latex:
\mforall{}[T,S:Type]. \mforall{}[A:T {}\mrightarrow{} \mBbbP{}]. \mforall{}[B:S {}\mrightarrow{} \mBbbP{}].
((\mexists{}t:T. (A t))
{}\mRightarrow{} (\mexists{}s:S. (B s))
{}\mRightarrow{} (\mforall{}p:T \mtimes{} S. Dec(predicate-and(A;B) p) \mLeftarrow{}{}\mRightarrow{} (\mforall{}x:T. Dec(A x)) \mwedge{} (\mforall{}y:S. Dec(B y))))
By
Latex:
(Auto THEN ExRepD)
Home
Index