Nuprl Definition : alttree
Tree(A) == ∀n:ℕ. ∀s:ℕn ⟶ T. ((↑(A n s)) ⇒ (∀i:ℕn. (↑(A i s))))
Definitions occuring in Statement :
int_seg: {i..j-},
nat: ℕ,
assert: ↑b,
all: ∀x:A. B[x],
implies: P ⇒ Q,
apply: f a,
function: x:A ⟶ B[x],
natural_number: $n
Definitions occuring in definition :
apply: f a,
assert: ↑b,
natural_number: $n,
int_seg: {i..j-},
all: ∀x:A. B[x],
implies: P ⇒ Q,
function: x:A ⟶ B[x],
nat: ℕ
FDL editor aliases :
alttree
Latex:
Tree(A) == \mforall{}n:\mBbbN{}. \mforall{}s:\mBbbN{}n {}\mrightarrow{} T. ((\muparrow{}(A n s)) {}\mRightarrow{} (\mforall{}i:\mBbbN{}n. (\muparrow{}(A i s))))
Date html generated:
2019_06_20-PM-02_46_07
Last ObjectModification:
2019_06_06-PM-01_27_03
Theory : fan-theorem
Home
Index