Step
*
of Lemma
fan-implies-barred-not-unbounded
∀[T:Type]. (Fan_d(T)
⇒ (∀A:(T List) ⟶ ℙ. (dbar(T;A)
⇒ (¬(down-closed(T;¬(A)) ∧ Unbounded(¬(A)))))))
BY
{ (Auto THEN (D 0 THENA Auto) THEN (With ⌜A⌝ (D 2)⋅ THENA Auto) THEN ThinTrivial THEN Auto) }
1
1. T : Type
2. A : (T List) ⟶ ℙ
3. dbar(T;A)
4. down-closed(T;¬(A))
5. Unbounded(¬(A))
6. ubar(T;A)
⊢ False
Latex:
Latex:
\mforall{}[T:Type]
(Fan\_d(T) {}\mRightarrow{} (\mforall{}A:(T List) {}\mrightarrow{} \mBbbP{}. (dbar(T;A) {}\mRightarrow{} (\mneg{}(down-closed(T;\mneg{}(A)) \mwedge{} Unbounded(\mneg{}(A)))))))
By
Latex:
(Auto THEN (D 0 THENA Auto) THEN (With \mkleeneopen{}A\mkleeneclose{} (D 2)\mcdot{} THENA Auto) THEN ThinTrivial THEN Auto)
Home
Index