Nuprl Definition : separation-space
SeparationSpace ==
"Point":Type
"#":{s:self."Point" ⟶ self."Point" ⟶ ℙ| ∀x:self."Point". (¬(s x 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 :
record+: record+,
record: record(x.T[x]),
top: Top,
universe: Type,
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
prop: ℙ,
not: ¬A,
all: ∀x:A. B[x],
implies: P ⇒ Q,
or: P ∨ Q,
apply: f a,
record-select: r.x,
token: "$token"
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))\}
"\#or":\mforall{}x,y,z:self."Point". ((self."\#" x y) {}\mRightarrow{} ((self."\#" x z) \mvee{} (self."\#" y z)))
Date html generated:
2019_10_31-AM-07_26_10
Last ObjectModification:
2019_09_19-PM-04_04_22
Theory : constructive!algebra
Home
Index