Nuprl Lemma : filter-interface-predecessors-lower-bound3

      ∀X:EClass(T). ∀P:E(X) ─→ 𝔹. ∀n:ℕ+. ∀f:ℕn ─→ {e:E(X)| ↑P[e]} .
        (∃e:{e:E(X)| ↑P[e]} (n ≤ ||filter(λe.P[e];≤(X)(e))||)) supposing 
           ((∀i,j:ℕn.  (loc(f i) loc(f j) ∈ Id)) and 
           Inj(ℕn;{e:E(X)| ↑P[e]} ;f))


Definitions occuring in Statement :  es-interface-predecessors: (X)(e) es-E-interface: E(X) eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) es-loc: loc(e) Id: Id filter: filter(P;l) length: ||as|| inject: Inj(A;B;f) nat_plus: + int_seg: {i..j-} assert: b bool: 𝔹 uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s] le: A ≤ B all: x:A. B[x] exists: x:A. B[x] set: {x:A| B[x]}  apply: a lambda: λx.A[x] function: x:A ─→ B[x] natural_number: $n universe: Type equal: t ∈ T
Lemmas :  es-E-interface_wf es-interface-subtype_rel2 es-E_wf event-ordering+_subtype event-ordering+_wf top_wf assert_wf int_seg_wf all_wf equal_wf Id_wf es-loc_wf inject_wf nat_plus_wf bool_wf eclass_wf last-event-of-set subtype_rel_dep_function le_wf length_wf filter_wf5 es-interface-predecessors_wf l_member_wf set_wf filter-interface-predecessors-lower-bound nat_plus_subtype_nat

            \mforall{}X:EClass(T).  \mforall{}P:E(X)  {}\mrightarrow{}  \mBbbB{}.  \mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}f:\mBbbN{}n  {}\mrightarrow{}  \{e:E(X)|  \muparrow{}P[e]\}  .
                (\mexists{}e:\{e:E(X)|  \muparrow{}P[e]\}  .  (n  \mleq{}  ||filter(\mlambda{}e.P[e];\mleq{}(X)(e))||))  supposing 
                      ((\mforall{}i,j:\mBbbN{}n.    (loc(f  i)  =  loc(f  j)))  and 
                      Inj(\mBbbN{}n;\{e:E(X)|  \muparrow{}P[e]\}  ;f))

Date html generated: 2015_07_21-PM-03_40_22
Last ObjectModification: 2015_01_27-PM-06_29_18

Home Index