Nuprl Lemma : rcc-subinterval
∀I:Interval. ∀a,b:ℝ. ([a, b] ⊆ I ⇐⇒ (a ≤ b) ⇒ ((a ∈ I) ∧ (b ∈ I)))
Proof
Definitions occuring in Statement :
subinterval: I ⊆ J ,
rccint: [l, u],
i-member: r ∈ I,
interval: Interval,
rleq: x ≤ y,
real: ℝ,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
implies: P ⇒ Q,
and: P ∧ Q
Definitions unfolded in proof :
subinterval: I ⊆ J ,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
and: P ∧ Q,
implies: P ⇒ Q,
member: t ∈ T,
i-member: r ∈ I,
rccint: [l, u],
uall: ∀[x:A]. B[x],
uimplies: b supposing a,
prop: ℙ,
so_lambda: λ2x.t[x],
so_apply: x[s],
rev_implies: P ⇐ Q,
guard: {T}
Lemmas referenced :
rleq_weakening_equal,
rleq_wf,
all_wf,
real_wf,
i-member_wf,
rccint_wf,
and_wf,
interval_wf,
i-member-between,
rleq_transitivity
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
lambdaFormation,
independent_pairFormation,
cut,
hypothesis,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesisEquality,
independent_functionElimination,
lemma_by_obid,
isectElimination,
because_Cache,
independent_isectElimination,
lambdaEquality,
functionEquality,
productElimination
Latex:
\mforall{}I:Interval. \mforall{}a,b:\mBbbR{}. ([a, b] \msubseteq{} I \mLeftarrow{}{}\mRightarrow{} (a \mleq{} b) {}\mRightarrow{} ((a \mmember{} I) \mwedge{} (b \mmember{} I)))
Date html generated:
2016_05_18-AM-08_50_08
Last ObjectModification:
2015_12_27-PM-11_45_18
Theory : reals
Home
Index