Nuprl Definition : inhabited-classrel
inhabited-classrel(eo;T;X;e) == ↓∃v:T. v ∈ X(e)
Definitions occuring in Statement :
classrel: v ∈ X(e),
exists: ∃x:A. B[x],
squash: ↓T
FDL editor aliases :
inhabited-classrel
inhabited-classrel(eo;T;X;e) == \mdownarrow{}\mexists{}v:T. v \mmember{} X(e)
Date html generated:
2015_07_17-PM-00_30_37
Last ObjectModification:
2012_02_25-PM-01_17_18
Home
Index