Nuprl Definition : topspace
Space == X:Type × E:X ⟶ X ⟶ ℙ × EquivRel(X;x,y.E x y)
Definitions occuring in Statement :
equiv_rel: EquivRel(T;x,y.E[x; y]),
prop: ℙ,
apply: f a,
function: x:A ⟶ B[x],
product: x:A × B[x],
universe: Type
Definitions occuring in definition :
apply: f a,
equiv_rel: EquivRel(T;x,y.E[x; y]),
prop: ℙ,
function: x:A ⟶ B[x],
product: x:A × B[x],
universe: Type
FDL editor aliases :
topspace
Latex:
Space == X:Type \mtimes{} E:X {}\mrightarrow{} X {}\mrightarrow{} \mBbbP{} \mtimes{} EquivRel(X;x,y.E x y)
Date html generated:
2018_07_29-AM-09_47_25
Last ObjectModification:
2018_06_21-AM-10_17_33
Theory : inner!product!spaces
Home
Index