Nuprl Lemma : iseg_filter

[T:Type]
  ∀P:T ⟶ 𝔹. ∀L_1,L_2:T List.  (L_2 ≤ filter(P;L_1)  (∃L_3:T List. (L_3 ≤ L_1 ∧ (L_2 filter(P;L_3) ∈ (T List)))))


Proof




Definitions occuring in Statement :  iseg: l1 ≤ l2 filter: filter(P;l) list: List bool: 𝔹 uall: [x:A]. B[x] all: x:A. B[x] exists: x:A. B[x] implies:  Q and: P ∧ Q function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] member: t ∈ T so_lambda: λ2x.t[x] implies:  Q prop: subtype_rel: A ⊆B so_apply: x[s] uimplies: supposing a and: P ∧ Q top: Top exists: x:A. B[x] cand: c∧ B iff: ⇐⇒ Q uiff: uiff(P;Q) bool: 𝔹 unit: Unit it: btrue: tt ifthenelse: if then else fi  bfalse: ff rev_implies:  Q squash: T true: True not: ¬A false: False
Lemmas referenced :  list_induction all_wf list_wf iseg_wf filter_wf5 subtype_rel_dep_function bool_wf l_member_wf subtype_rel_self set_wf exists_wf equal_wf filter_nil_lemma filter_cons_lemma nil_wf iseg_weakening iseg_nil assert_of_null equal-wf-T-base assert_wf bnot_wf not_wf eqtt_to_assert uiff_transitivity eqff_to_assert assert_of_bnot cons_wf nil_iseg equal-wf-base-T cons_iseg
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut thin introduction extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality sqequalRule lambdaEquality hypothesis functionEquality applyEquality because_Cache setEquality independent_isectElimination setElimination rename productEquality independent_functionElimination dependent_functionElimination isect_memberEquality voidElimination voidEquality universeEquality dependent_pairFormation independent_pairFormation productElimination equalityTransitivity equalitySymmetry baseClosed unionElimination equalityElimination cumulativity imageElimination natural_numberEquality imageMemberEquality

Latex:
\mforall{}[T:Type]
    \mforall{}P:T  {}\mrightarrow{}  \mBbbB{}.  \mforall{}L$_{1}$,L$_{2}$:T  List.    (L$_{2\mbackslash{}ff\000C7d$  \mleq{}  filter(P;L$_{1}$)  {}\mRightarrow{}  (\mexists{}L$_{3}$:T  List.  (L$\mbackslash{}ff5\000Cf{3}$  \mleq{}  L$_{1}$  \mwedge{}  (L$_{2}$  =  filter(P;L$\mbackslash{}ff5\000Cf{3}$)))))



Date html generated: 2019_06_20-PM-01_29_18
Last ObjectModification: 2018_09_17-PM-06_52_30

Theory : list_1


Home Index