### Nuprl Lemma : partition-refines_weakening

`∀I:Interval. ∀P,Q:partition(I).  ((P = Q ∈ partition(I)) `` P refines Q) supposing icompact(I)`

Proof

Definitions occuring in Statement :  partition-refines: `P refines Q` partition: `partition(I)` icompact: `icompact(I)` interval: `Interval` uimplies: `b supposing a` all: `∀x:A. B[x]` implies: `P `` Q` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uimplies: `b supposing a` implies: `P `` Q` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` partition-refines: `P refines Q` partition: `partition(I)`
Lemmas referenced :  partition-refines_wf equal_wf partition_wf icompact_wf interval_wf frs-refines_weakening
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation isect_memberFormation cut hypothesis thin hyp_replacement equalitySymmetry Error :applyLambdaEquality,  introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination hypothesisEquality independent_isectElimination sqequalRule isectElimination setElimination rename because_Cache independent_functionElimination

Latex:
\mforall{}I:Interval.  \mforall{}P,Q:partition(I).    ((P  =  Q)  {}\mRightarrow{}  P  refines  Q)  supposing  icompact(I)

Date html generated: 2016_10_26-AM-09_41_26
Last ObjectModification: 2016_07_12-AM-08_22_08

Theory : reals

Home Index