Nuprl Definition : loset
LOSet == {s:POSet{i}| Connex(|s|;x,y.x ≤ y)}
Definitions occuring in Statement :
poset: POSet{i},
set_leq: a ≤ b,
set_car: |p|,
connex: Connex(T;x,y.R[x; y]),
set: {x:A| B[x]}
Definitions occuring in definition :
set: {x:A| B[x]} ,
poset: POSet{i},
connex: Connex(T;x,y.R[x; y]),
set_car: |p|,
set_leq: a ≤ b
Latex:
LOSet == \{s:POSet\{i\}| Connex(|s|;x,y.x \mleq{} y)\}
Date html generated:
2016_05_15-PM-00_05_13
Last ObjectModification:
2015_09_23-AM-06_24_06
Theory : sets_1
Home
Index