Nuprl Definition : altpath
IsPath(A;f) == ∀n:ℕ. (↑(A n f))
Definitions occuring in Statement :
nat: ℕ,
assert: ↑b,
all: ∀x:A. B[x],
apply: f a
Definitions occuring in definition :
apply: f a,
assert: ↑b,
nat: ℕ,
all: ∀x:A. B[x]
FDL editor aliases :
altpath
Latex:
IsPath(A;f) == \mforall{}n:\mBbbN{}. (\muparrow{}(A n f))
Date html generated:
2019_06_20-PM-02_46_22
Last ObjectModification:
2019_06_06-PM-01_46_20
Theory : fan-theorem
Home
Index