Nuprl Definition : ss-free-homotopic
ss-free-homotopic(X;a;b) == ∃p:Point(Path(X)). (p@r0 ≡ a ∧ p@r1 ≡ b)
Definitions occuring in Statement :
path-at: p@t,
path-ss: Path(X),
ss-eq: x ≡ y,
ss-point: Point(ss),
int-to-real: r(n),
exists: ∃x:A. B[x],
and: P ∧ Q,
natural_number: $n
Definitions occuring in definition :
exists: ∃x:A. B[x],
ss-point: Point(ss),
path-ss: Path(X),
and: P ∧ Q,
ss-eq: x ≡ y,
path-at: p@t,
int-to-real: r(n),
natural_number: $n
FDL editor aliases :
ss-free-homotopic
Latex:
ss-free-homotopic(X;a;b) == \mexists{}p:Point(Path(X)). (p@r0 \mequiv{} a \mwedge{} p@r1 \mequiv{} b)
Date html generated:
2020_05_20-PM-01_20_21
Last ObjectModification:
2018_07_05-PM-03_16_10
Theory : intuitionistic!topology
Home
Index