Nuprl Lemma : partition-refines-cons

∀I:Interval
  (icompact(I)
  ⇒ (∀a:ℝ. ∀bs:ℝ List.
        (partitions(I;[a / bs])
        ⇒ (0 < ||bs|| ⇒ (a < hd(bs)))
        ⇒ (∀p:partition(I)
              (p refines [a / bs]
              ⇒ (∃q:partition([left-endpoint(I), a])
                   ∃r:partition([a, right-endpoint(I)])
                    (q refines []
                    ∧ r refines bs
                    ∧ (∃x:ℝ. ((x = a) ∧ (p = (q @ [x / r]) ∈ (ℝ List))))
                    ∧ ||r|| + ||q|| < ||p||
                    ∧ (∀x:partition-choice(full-partition(I;p))
                         (is-partition-choice(full-partition([left-endpoint(I), a];q);x)
                         ∧ is-partition-choice(full-partition([a, right-endpoint(I)];r);λi.(x (i + ||q|| + 1))))))))))))


Proof



Definitions occuring in Statement :  partition-refines: P refines Q,  partition-choice: partition-choice(p),  is-partition-choice: is-partition-choice(p;x),  full-partition: full-partition(I;p),  partition: partition(I),  partitions: partitions(I;p),  icompact: icompact(I),  rccint: [l, u],  right-endpoint: right-endpoint(I),  left-endpoint: left-endpoint(I),  interval: Interval,  rless: x < y,  req: x = y,  real: ℝ,  length: ||as||,  append: as @ bs,  hd: hd(l),  cons: [a / b],  nil: [],  list: T List,  less_than: a < b,  all: ∀x:A. B[x],  exists: ∃x:A. B[x],  implies: P ⇒ Q,  and: P ∧ Q,  apply: f a,  lambda: λx.A[x],  add: n + m,  natural_number: $n,  equal: s = t ∈ T
Definitions unfolded in proof :  all: ∀x:A. B[x],  uall: ∀[x:A]. B[x],  member: t ∈ T,  implies: P ⇒ Q,  uimplies: b supposing a,  and: P ∧ Q,  partition-refines: P refines Q,  frs-refines: frs-refines(p;q),  l_all: (∀x∈L.P[x]),  int_seg: {i..j-},  lelt: i ≤ j < k,  le: A ≤ B,  less_than': less_than'(a;b),  false: False,  not: ¬A,  nat_plus: ℕ+,  decidable: Dec(P),  or: P ∨ Q,  satisfiable_int_formula: satisfiable_int_formula(fmla),  exists: ∃x:A. B[x],  prop: ℙ,  guard: {T},  uiff: uiff(P;Q),  select: L[n],  cons: [a / b],  l_exists: (∃x∈L. P[x]),  partition: partition(I),  full-partition: full-partition(I;p),  subtype_rel: A ⊆r B,  int_iseg: {i...j},  so_lambda: λ2x.t[x],  so_apply: x[s],  less_than: a < b,  squash: ↓T,  true: True,  iff: P ⇐⇒ Q,  rev_implies: P ⇐ Q,  ge: i ≥ j ,  icompact: icompact(I),  cand: A c∧ B,  nat: ℕ,  bool: 𝔹,  unit: Unit,  it: ⋅,  btrue: tt,  ifthenelse: if b then t else f fi ,  bfalse: ff,  sq_type: SQType(T),  bnot: ¬bb,  assert: ↑b,  so_apply: x[s1;s2],  top: Top,  so_lambda: λ2x y.t[x; y],  nil: [],  subtract: n - m,  frs-non-dec: frs-non-dec(L),  sq_stable: SqStable(P),  partitions: partitions(I;p),  rleq: x ≤ y,  real: ℝ,  sq_exists: ∃x:A [B[x]],  rless: x < y,  so_apply: x[s1;s2;s3],  so_lambda: so_lambda3,  append: as @ bs,  partition-choice: partition-choice(p),  is-partition-choice: is-partition-choice(p;x),  i-member: r ∈ I,  rccint: [l, u],  rev_uimplies: rev_uimplies(P;Q),  rge: x ≥ y,  endpoints: endpoints(I),  left-endpoint: left-endpoint(I)
Latex:
\mforall{}I:Interval
    (icompact(I)
    {}\mRightarrow{}  (\mforall{}a:\mBbbR{}.  \mforall{}bs:\mBbbR{}  List.
                (partitions(I;[a  /  bs])
                {}\mRightarrow{}  (0  <  ||bs||  {}\mRightarrow{}  (a  <  hd(bs)))
                {}\mRightarrow{}  (\mforall{}p:partition(I)
                            (p  refines  [a  /  bs]
                            {}\mRightarrow{}  (\mexists{}q:partition([left-endpoint(I),  a])
                                      \mexists{}r:partition([a,  right-endpoint(I)])
                                        (q  refines  []
                                        \mwedge{}  r  refines  bs
                                        \mwedge{}  (\mexists{}x:\mBbbR{}.  ((x  =  a)  \mwedge{}  (p  =  (q  @  [x  /  r]))))
                                        \mwedge{}  ...)))))))


Date html generated: 2020_05_20-AM-11_38_36
Last ObjectModification: 2020_01_03-AM-00_15_56

Theory : reals


Home Index