### Nuprl Lemma : rfun_subtype_1

`∀[a,b,c:ℝ].  ((a ≤ c) `` (c ≤ b) `` ([a, b] ⟶ℝ ⊆r [a, c] ⟶ℝ))`

Proof

Definitions occuring in Statement :  rfun: `I ⟶ℝ` rccint: `[l, u]` rleq: `x ≤ y` real: `ℝ` subtype_rel: `A ⊆r B` uall: `∀[x:A]. B[x]` implies: `P `` Q`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` implies: `P `` Q` subtype_rel: `A ⊆r B` prop: `ℙ` rfun: `I ⟶ℝ` all: `∀x:A. B[x]` top: `Top` and: `P ∧ Q` cand: `A c∧ B` guard: `{T}` uimplies: `b supposing a`
Lemmas referenced :  rfun_wf rccint_wf rleq_wf real_wf i-member_wf member_rccint_lemma rleq_transitivity
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation lambdaEquality extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis sqequalRule dependent_functionElimination axiomEquality because_Cache isect_memberEquality functionExtensionality setEquality setElimination rename voidElimination voidEquality applyEquality productElimination independent_pairFormation independent_isectElimination dependent_set_memberEquality productEquality

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

Date html generated: 2016_10_26-AM-09_29_48
Last ObjectModification: 2016_08_20-AM-10_16_09

Theory : reals

Home Index