Nuprl Lemma : ifun_subtype_2

[a,b,c:ℝ].  ((a ≤ c)  (c ≤ b)  ({f:[a, b] ⟶ℝifun(f;[a, b])}  ⊆{f:[c, b] ⟶ℝifun(f;[c, b])} ))


Proof




Definitions occuring in Statement :  ifun: ifun(f;I) rfun: I ⟶ℝ rccint: [l, u] rleq: x ≤ y real: subtype_rel: A ⊆B uall: [x:A]. B[x] implies:  Q set: {x:A| B[x]} 
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T implies:  Q subtype_rel: A ⊆B uimplies: supposing a all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q prop: guard: {T} ifun: ifun(f;I) real-fun: real-fun(f;a;b) top: Top so_lambda: λ2x.t[x] so_apply: x[s] cand: c∧ B
Lemmas referenced :  rfun_subtype_2 ifun_wf rccint_wf rccint-icompact rfun_wf rleq_transitivity rleq_wf real_wf member_rccint_lemma left_endpoint_rccint_lemma right_endpoint_rccint_lemma subtype_rel_sets set_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation lambdaEquality setElimination thin rename dependent_set_memberEquality hypothesisEquality applyEquality extract_by_obid sqequalHypSubstitution isectElimination independent_functionElimination hypothesis sqequalRule because_Cache independent_isectElimination dependent_functionElimination productElimination setEquality axiomEquality isect_memberEquality voidElimination voidEquality productEquality independent_pairFormation

Latex:
\mforall{}[a,b,c:\mBbbR{}].
    ((a  \mleq{}  c)  {}\mRightarrow{}  (c  \mleq{}  b)  {}\mRightarrow{}  (\{f:[a,  b]  {}\mrightarrow{}\mBbbR{}|  ifun(f;[a,  b])\}    \msubseteq{}r  \{f:[c,  b]  {}\mrightarrow{}\mBbbR{}|  ifun(f;[c,  b])\}  ))



Date html generated: 2016_10_26-AM-09_48_33
Last ObjectModification: 2016_08_20-AM-10_19_17

Theory : reals


Home Index