Nuprl Lemma : partitions_wf

[I:Interval]. ∀[p:ℝ List].  partitions(I;p) ∈ ℙ supposing icompact(I)


Proof




Definitions occuring in Statement :  partitions: partitions(I;p) icompact: icompact(I) interval: Interval real: list: List uimplies: supposing a uall: [x:A]. B[x] prop: member: t ∈ T
Definitions unfolded in proof :  icompact: icompact(I) bfalse: ff cons: [a b] squash: T less_than: a < b so_apply: x[s1;s2] top: Top so_lambda: λ2y.t[x; y] it: nil: [] select: L[n] btrue: tt ifthenelse: if then else fi  assert: b or: P ∨ Q all: x:A. B[x] not: ¬A false: False less_than': less_than'(a;b) le: A ≤ B implies:  Q and: P ∧ Q prop: partitions: partitions(I;p) uimplies: supposing a member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  interval_wf list_wf icompact_wf right-endpoint_wf length_of_cons_lemma null_cons_lemma product_subtype_list base_wf stuck-spread length_of_nil_lemma null_nil_lemma list-cases last_wf false_wf select_wf left-endpoint_wf rleq_wf real_wf length_wf less_than_wf frs-non-dec_wf
Rules used in proof :  equalitySymmetry equalityTransitivity axiomEquality hypothesis_subsumption promote_hyp productElimination imageElimination voidEquality voidElimination isect_memberEquality baseClosed unionElimination dependent_functionElimination lambdaFormation independent_pairFormation independent_isectElimination because_Cache natural_numberEquality functionEquality hypothesis hypothesisEquality thin isectElimination sqequalHypSubstitution extract_by_obid productEquality sqequalRule cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[I:Interval].  \mforall{}[p:\mBbbR{}  List].    partitions(I;p)  \mmember{}  \mBbbP{}  supposing  icompact(I)



Date html generated: 2018_05_22-PM-02_06_02
Last ObjectModification: 2018_05_21-AM-00_18_27

Theory : reals


Home Index