### Nuprl Lemma : full-partition_wf

`∀[I:Interval]. ∀[p:partition(I)]. (full-partition(I;p) ∈ ℝ List) supposing icompact(I)`

Proof

Definitions occuring in Statement :  full-partition: `full-partition(I;p)` partition: `partition(I)` icompact: `icompact(I)` interval: `Interval` real: `ℝ` list: `T List` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` member: `t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` full-partition: `full-partition(I;p)` partition: `partition(I)` prop: `ℙ` icompact: `icompact(I)` and: `P ∧ Q`
Lemmas referenced :  cons_wf real_wf left-endpoint_wf append_wf right-endpoint_wf nil_wf partition_wf icompact_wf interval_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesis hypothesisEquality independent_isectElimination because_Cache setElimination rename axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality productElimination

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

Date html generated: 2016_05_18-AM-08_55_49
Last ObjectModification: 2015_12_27-PM-11_38_18

Theory : reals

Home Index