Nuprl Lemma : inf-range-no-mc
∀I:{I:Interval| icompact(I)} . ∀f:{f:I ⟶ℝ| ifun(f;I)} . ∃y:ℝ. inf(f(x)(x∈I)) = y
Proof
Definitions occuring in Statement :
ifun: ifun(f;I),
rrange: f[x](x∈I),
icompact: icompact(I),
r-ap: f(x),
rfun: I ⟶ℝ,
interval: Interval,
inf: inf(A) = b,
real: ℝ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
set: {x:A| B[x]}
Definitions unfolded in proof :
so_apply: x[s],
uimplies: b supposing a,
so_lambda: λ2x.t[x],
uall: ∀[x:A]. B[x],
prop: ℙ,
squash: ↓T,
sq_stable: SqStable(P),
implies: P ⇒ Q,
member: t ∈ T,
all: ∀x:A. B[x]
Lemmas referenced :
icompact_wf,
interval_wf,
ifun_wf,
rfun_wf,
set_wf,
sq_stable__icompact,
ifun-continuous,
inf-range
Rules used in proof :
independent_isectElimination,
lambdaEquality,
isectElimination,
imageElimination,
baseClosed,
imageMemberEquality,
sqequalRule,
because_Cache,
independent_functionElimination,
hypothesis,
rename,
setElimination,
hypothesisEquality,
thin,
dependent_functionElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
cut,
lambdaFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}I:\{I:Interval| icompact(I)\} . \mforall{}f:\{f:I {}\mrightarrow{}\mBbbR{}| ifun(f;I)\} . \mexists{}y:\mBbbR{}. inf(f(x)(x\mmember{}I)) = y
Date html generated:
2018_07_29-AM-09_42_17
Last ObjectModification:
2018_06_29-PM-04_31_44
Theory : reals
Home
Index