Nuprl Lemma : range-inf-property
∀I:{I:Interval| icompact(I)} . ∀f:I ⟶ℝ. ∀mc:f[x] continuous for x ∈ I. inf(f[x](x∈I)) = inf{f[x]|x ∈ I}
Proof
Definitions occuring in Statement :
range-inf: inf{f[x]|x ∈ I},
continuous: f[x] continuous for x ∈ I,
rrange: f[x](x∈I),
icompact: icompact(I),
rfun: I ⟶ℝ,
interval: Interval,
inf: inf(A) = b,
so_apply: x[s],
all: ∀x:A. B[x],
set: {x:A| B[x]}
Definitions unfolded in proof :
so_apply: x[s],
all: ∀x:A. B[x],
range-inf: inf{f[x]|x ∈ I},
member: t ∈ T,
subtype_rel: A ⊆r B,
uall: ∀[x:A]. B[x],
so_lambda: λ2x.t[x],
implies: P ⇒ Q,
prop: ℙ,
label: ...$L... t,
rfun: I ⟶ℝ,
uimplies: b supposing a,
sq_stable: SqStable(P),
squash: ↓T,
exists: ∃x:A. B[x],
r-ap: f(x),
pi1: fst(t)
Latex:
\mforall{}I:\{I:Interval| icompact(I)\} . \mforall{}f:I {}\mrightarrow{}\mBbbR{}. \mforall{}mc:f[x] continuous for x \mmember{} I.
inf(f[x](x\mmember{}I)) = inf\{f[x]|x \mmember{} I\}
Date html generated:
2020_05_20-PM-00_17_32
Last ObjectModification:
2020_01_03-PM-00_14_56
Theory : reals
Home
Index