Nuprl Lemma : real-continuity
∀a,b:ℝ. ∀f:[a, b] ⟶ℝ. real-cont(f;a;b) supposing real-fun(f;a;b) supposing a ≤ b
Proof
Definitions occuring in Statement :
real-cont: real-cont(f;a;b),
real-fun: real-fun(f;a;b),
rfun: I ⟶ℝ,
rccint: [l, u],
rleq: x ≤ y,
real: ℝ,
uimplies: b supposing a,
all: ∀x:A. B[x]
Definitions unfolded in proof :
all: ∀x:A. B[x],
uimplies: b supposing a,
member: t ∈ T,
rleq: x ≤ y,
rnonneg: rnonneg(x),
uall: ∀[x:A]. B[x],
le: A ≤ B,
and: P ∧ Q,
real-fun: real-fun(f;a;b),
implies: P ⇒ Q,
rfun: I ⟶ℝ,
prop: ℙ,
mcompact: mcompact(X;d),
subtype_rel: A ⊆r B,
top: Top,
mfun: FUN(X ⟶ Y),
is-mfun: f:FUN(X;Y),
so_apply: x[s],
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
rmetric: rmetric(),
m-unif-cont: UC(f:X ⟶ Y),
real-cont: real-cont(f;a;b),
mdist: mdist(d;x;y)
Latex:
\mforall{}a,b:\mBbbR{}. \mforall{}f:[a, b] {}\mrightarrow{}\mBbbR{}. real-cont(f;a;b) supposing real-fun(f;a;b) supposing a \mleq{} b
Date html generated:
2020_05_20-PM-00_04_23
Last ObjectModification:
2019_11_25-PM-00_24_41
Theory : reals
Home
Index