Nuprl Definition : path-comp-rel
path-comp-rel(X;f;g;h) ==
(∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . h@t ≡ f@r(2) * t) ∧ (∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . h@t ≡ g@(r(2) * t) - r1)
Definitions occuring in Statement :
path-at: p@t,
ss-eq: x ≡ y,
rccint: [l, u],
i-member: r ∈ I,
rdiv: (x/y),
rsub: x - y,
rmul: a * b,
int-to-real: r(n),
real: ℝ,
all: ∀x:A. B[x],
and: P ∧ Q,
set: {x:A| B[x]} ,
natural_number: $n
Definitions occuring in definition :
and: P ∧ Q,
all: ∀x:A. B[x],
set: {x:A| B[x]} ,
real: ℝ,
i-member: r ∈ I,
rccint: [l, u],
rdiv: (x/y),
ss-eq: x ≡ y,
path-at: p@t,
rsub: x - y,
rmul: a * b,
int-to-real: r(n),
natural_number: $n
FDL editor aliases :
path-comp-rel
Latex:
path-comp-rel(X;f;g;h) ==
(\mforall{}t:\{x:\mBbbR{}| x \mmember{} [r0, (r1/r(2))]\} . h@t \mequiv{} f@r(2) * t)
\mwedge{} (\mforall{}t:\{x:\mBbbR{}| x \mmember{} [(r1/r(2)), r1]\} . h@t \mequiv{} g@(r(2) * t) - r1)
Date html generated:
2020_05_20-PM-01_20_40
Last ObjectModification:
2018_06_29-PM-05_47_43
Theory : intuitionistic!topology
Home
Index