### 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