### Nuprl Lemma : rfun-eq_wf

`∀[I:Interval]. ∀[f,g:I ⟶ℝ].  (rfun-eq(I;f;g) ∈ ℙ)`

Proof

Definitions occuring in Statement :  rfun-eq: `rfun-eq(I;f;g)` rfun: `I ⟶ℝ` interval: `Interval` uall: `∀[x:A]. B[x]` prop: `ℙ` member: `t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` rfun-eq: `rfun-eq(I;f;g)` prop: `ℙ` so_lambda: `λ2x.t[x]` all: `∀x:A. B[x]` uimplies: `b supposing a` so_apply: `x[s]`
Lemmas referenced :  all_wf real_wf i-member_wf req_wf r-ap_wf rfun_wf interval_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin setEquality hypothesis hypothesisEquality lambdaEquality lambdaFormation setElimination rename independent_isectElimination because_Cache axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality

Latex:
\mforall{}[I:Interval].  \mforall{}[f,g:I  {}\mrightarrow{}\mBbbR{}].    (rfun-eq(I;f;g)  \mmember{}  \mBbbP{})

Date html generated: 2016_05_18-AM-08_42_10
Last ObjectModification: 2015_12_27-PM-11_51_03

Theory : reals

Home Index