Nuprl Lemma : rat-interval-third_wf

[p:ℝ]. ∀[I:ℚInterval].  (rat-interval-third(p;I) ∈ ℙ)


Proof




Definitions occuring in Statement :  rat-interval-third: rat-interval-third(p;I) real: uall: [x:A]. B[x] prop: member: t ∈ T rational-interval: Interval
Definitions unfolded in proof :  true: True less_than': less_than'(a;b) squash: T less_than: a < b rev_implies:  Q iff: ⇐⇒ Q or: P ∨ Q guard: {T} rneq: x ≠ y uimplies: supposing a and: P ∧ Q prop: implies:  Q rational-interval: Interval top: Top all: x:A. B[x] rat-interval-third: rat-interval-third(p;I) member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  real_wf rational-interval_wf rless_wf rless-int int-to-real_wf rmul_wf radd_wf rdiv_wf req_wf or_wf rat2real_wf rleq_wf istype-void member_rccint_lemma
Rules used in proof :  inhabitedIsType isectIsTypeImplies equalitySymmetry equalityTransitivity axiomEquality universeIsType baseClosed imageMemberEquality independent_pairFormation independent_functionElimination inrFormation_alt independent_isectElimination natural_numberEquality closedConclusion because_Cache hypothesisEquality isectElimination productEquality functionEquality productElimination hypothesis voidElimination isect_memberEquality_alt thin dependent_functionElimination sqequalHypSubstitution extract_by_obid sqequalRule cut introduction isect_memberFormation_alt sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[p:\mBbbR{}].  \mforall{}[I:\mBbbQ{}Interval].    (rat-interval-third(p;I)  \mmember{}  \mBbbP{})



Date html generated: 2019_10_31-AM-06_03_40
Last ObjectModification: 2019_10_30-PM-01_29_44

Theory : real!vectors


Home Index