Nuprl Definition : separation-space
SeparationSpace ==
"Point":Type
"#":{s:self."Point" ⟶ self."Point" ⟶ ℙ| ∀x:self."Point". (¬(s x x))}
"#symm":∀x,y:self."Point". ((self."#" x y) ⇒ (self."#" y x))
"#or":∀x,y,z:self."Point". ((self."#" x y) ⇒ ((self."#" x z) ∨ (self."#" y z)))
Definitions occuring in Statement :
top: Top,
prop: ℙ,
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
or: P ∨ Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
token: "$token",
universe: Type,
record-select: r.x,
record+: record+,
record: record(x.T[x])
Definitions occuring in definition :
token: "$token",
record-select: r.x,
apply: f a,
or: P ∨ Q,
implies: P ⇒ Q,
all: ∀x:A. B[x],
not: ¬A,
prop: ℙ,
function: x:A ⟶ B[x],
set: {x:A| B[x]} ,
universe: Type,
top: Top,
record: record(x.T[x]),
record+: record+
FDL editor aliases :
sep-s
Latex:
SeparationSpace ==
"Point":Type
"\#":\{s:self."Point" {}\mrightarrow{} self."Point" {}\mrightarrow{} \mBbbP{}| \mforall{}x:self."Point". (\mneg{}(s x x))\}
"\#symm":\mforall{}x,y:self."Point". ((self."\#" x y) {}\mRightarrow{} (self."\#" y x))
"\#or":\mforall{}x,y,z:self."Point". ((self."\#" x y) {}\mRightarrow{} ((self."\#" x z) \mvee{} (self."\#" y z)))
Date html generated:
2016_11_08-AM-09_10_40
Last ObjectModification:
2016_10_31-AM-11_00_14
Theory : inner!product!spaces
Home
Index