Nuprl Definition : almost-full
almost-full(T;n;R) == ∃p:wfd-tree(T). tree-secures(T;[[R]];p)
Wellformedness Lemmas :
almost-full_wf
Definitions occuring in Statement :
tree-secures: tree-secures(T;A;p),
nary-rel-predicate: [[R]],
wfd-tree: wfd-tree(T),
exists: ∃x:A. B[x]
Definitions occuring in definition :
exists: ∃x:A. B[x],
wfd-tree: wfd-tree(T),
tree-secures: tree-secures(T;A;p),
nary-rel-predicate: [[R]]
FDL editor aliases :
almost-full
Latex:
almost-full(T;n;R) == \mexists{}p:wfd-tree(T). tree-secures(T;[[R]];p)
Date html generated:
2016_05_14-PM-04_07_33
Last ObjectModification:
2015_09_22-PM-06_02_08
Theory : fan-theorem
Home
Index