Nuprl Definition : bar-separation
BarSep(T;S) ==
∀A:(T List) ⟶ ℙ. ∀B:(S List) ⟶ ℙ. (Decidable(A) ⇒ Decidable(B) ⇒ jbar(T;S;A;B) ⇒ (tbar(T;A) ∨ tbar(S;B)))
Definitions occuring in Statement :
jbar: jbar(T;S;X;Y),
tbar: tbar(T;X),
dec-predicate: Decidable(X),
list: T List,
prop: ℙ,
all: ∀x:A. B[x],
implies: P ⇒ Q,
or: P ∨ Q,
function: x:A ⟶ B[x]
Definitions occuring in definition :
all: ∀x:A. B[x],
function: x:A ⟶ B[x],
prop: ℙ,
dec-predicate: Decidable(X),
list: T List,
implies: P ⇒ Q,
jbar: jbar(T;S;X;Y),
or: P ∨ Q,
tbar: tbar(T;X)
FDL editor aliases :
bar-separation
Latex:
BarSep(T;S) ==
\mforall{}A:(T List) {}\mrightarrow{} \mBbbP{}. \mforall{}B:(S List) {}\mrightarrow{} \mBbbP{}.
(Decidable(A) {}\mRightarrow{} Decidable(B) {}\mRightarrow{} jbar(T;S;A;B) {}\mRightarrow{} (tbar(T;A) \mvee{} tbar(S;B)))
Date html generated:
2016_05_14-PM-04_09_23
Last ObjectModification:
2015_09_22-PM-06_02_17
Theory : fan-theorem
Home
Index