### Nuprl Lemma : rset-member-rrange

`∀I:Interval. ∀[f:I ⟶ℝ]. ∀r:ℝ. ((r ∈ I) `` (f[r] ∈ f[x](x∈I)))`

Proof

Definitions occuring in Statement :  rrange: `f[x](x∈I)` rfun: `I ⟶ℝ` i-member: `r ∈ I` interval: `Interval` rset-member: `x ∈ A` real: `ℝ` uall: `∀[x:A]. B[x]` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` implies: `P `` Q` rrange: `f[x](x∈I)` rset-member: `x ∈ A` exists: `∃x:A. B[x]` member: `t ∈ T` and: `P ∧ Q` cand: `A c∧ B` so_apply: `x[s]` rfun: `I ⟶ℝ` prop: `ℙ` uimplies: `b supposing a`
Lemmas referenced :  req_weakening i-member_wf req_wf real_wf rfun_wf interval_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation isect_memberFormation dependent_pairFormation hypothesisEquality cut hypothesis independent_pairFormation lemma_by_obid sqequalHypSubstitution isectElimination thin applyEquality dependent_set_memberEquality because_Cache independent_isectElimination productEquality

Latex:
\mforall{}I:Interval.  \mforall{}[f:I  {}\mrightarrow{}\mBbbR{}].  \mforall{}r:\mBbbR{}.  ((r  \mmember{}  I)  {}\mRightarrow{}  (f[r]  \mmember{}  f[x](x\mmember{}I)))

Date html generated: 2016_05_18-AM-09_08_27
Last ObjectModification: 2015_12_27-PM-11_31_00

Theory : reals

Home Index