Nuprl Definition : dfan
Fan_d(T) == ∀X:(T List) ⟶ ℙ. (dbar(T;X) ⇒ ubar(T;X))
Definitions occuring in Statement :
dbar: dbar(T;X),
ubar: ubar(T;X),
list: T List,
prop: ℙ,
all: ∀x:A. B[x],
implies: P ⇒ Q,
function: x:A ⟶ B[x]
Definitions occuring in definition :
all: ∀x:A. B[x],
function: x:A ⟶ B[x],
list: T List,
prop: ℙ,
implies: P ⇒ Q,
dbar: dbar(T;X),
ubar: ubar(T;X)
FDL editor aliases :
dfan
Latex:
Fan\_d(T) == \mforall{}X:(T List) {}\mrightarrow{} \mBbbP{}. (dbar(T;X) {}\mRightarrow{} ubar(T;X))
Date html generated:
2016_05_14-PM-04_09_21
Last ObjectModification:
2015_09_22-PM-06_02_16
Theory : fan-theorem
Home
Index