Nuprl Definition : path-comp-property
path-comp-property(X) == ∀f,g:Point(Path(X)). (f@r1 ≡ g@r0 ⇒ (∃h:Point(Path(X)). path-comp-rel(X;f;g;h)))
Definitions occuring in Statement :
path-comp-rel: path-comp-rel(X;f;g;h),
path-at: p@t,
path-ss: Path(X),
ss-eq: x ≡ y,
ss-point: Point(ss),
int-to-real: r(n),
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
natural_number: $n
Definitions occuring in definition :
all: ∀x:A. B[x],
implies: P ⇒ Q,
ss-eq: x ≡ y,
path-at: p@t,
int-to-real: r(n),
natural_number: $n,
exists: ∃x:A. B[x],
ss-point: Point(ss),
path-ss: Path(X),
path-comp-rel: path-comp-rel(X;f;g;h)
FDL editor aliases :
path-comp-property
Latex:
path-comp-property(X) ==
\mforall{}f,g:Point(Path(X)). (f@r1 \mequiv{} g@r0 {}\mRightarrow{} (\mexists{}h:Point(Path(X)). path-comp-rel(X;f;g;h)))
Date html generated:
2020_05_20-PM-01_20_44
Last ObjectModification:
2018_06_29-PM-05_47_45
Theory : intuitionistic!topology
Home
Index