Nuprl Definition : altbarsep
BarSep(T;S) == ∀A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹. ∀B:n:ℕ ⟶ (ℕn ⟶ S) ⟶ 𝔹. (jbar(A;B) ⇒ (bar(A) ∨ bar(B)))
Definitions occuring in Statement :
altjbar: jbar(X;Y),
altbar: bar(X),
int_seg: {i..j-},
nat: ℕ,
bool: 𝔹,
all: ∀x:A. B[x],
implies: P ⇒ Q,
or: P ∨ Q,
function: x:A ⟶ B[x],
natural_number: $n
Definitions occuring in definition :
altbar: bar(X),
or: P ∨ Q,
altjbar: jbar(X;Y),
implies: P ⇒ Q,
bool: 𝔹,
natural_number: $n,
int_seg: {i..j-},
function: x:A ⟶ B[x],
nat: ℕ,
all: ∀x:A. B[x]
FDL editor aliases :
altbarsep
Latex:
BarSep(T;S) ==
\mforall{}A:n:\mBbbN{} {}\mrightarrow{} (\mBbbN{}n {}\mrightarrow{} T) {}\mrightarrow{} \mBbbB{}. \mforall{}B:n:\mBbbN{} {}\mrightarrow{} (\mBbbN{}n {}\mrightarrow{} S) {}\mrightarrow{} \mBbbB{}. (jbar(A;B) {}\mRightarrow{} (bar(A) \mvee{} bar(B)))
Date html generated:
2019_06_20-PM-02_46_15
Last ObjectModification:
2019_06_06-AM-11_03_53
Theory : fan-theorem
Home
Index