Nuprl Lemma : rfun_subtype_1

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


Proof




Definitions occuring in Statement :  rfun: I ⟶ℝ rccint: [l, u] rleq: x ≤ y real: subtype_rel: A ⊆B uall: [x:A]. B[x] implies:  Q
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T implies:  Q subtype_rel: A ⊆B prop: rfun: I ⟶ℝ all: x:A. B[x] top: Top and: P ∧ Q cand: c∧ B guard: {T} uimplies: 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