Nuprl Lemma : filter_iseg2

[T:Type]. ∀L2,L1:T List. ∀P:{x:T| (x ∈ L2)}  ⟶ 𝔹.  (L1 ≤ L2  filter(P;L1) ≤ filter(P;L2))


Proof




Definitions occuring in Statement :  iseg: l1 ≤ l2 l_member: (x ∈ l) filter: filter(P;l) list: List bool: 𝔹 uall: [x:A]. B[x] all: x:A. B[x] implies:  Q set: {x:A| B[x]}  function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] member: t ∈ T so_lambda: λ2x.t[x] prop: implies:  Q subtype_rel: A ⊆B so_apply: x[s] uimplies: supposing a istype: istype(T) top: Top iff: ⇐⇒ Q and: P ∧ Q uiff: uiff(P;Q) rev_implies:  Q or: P ∨ Q bool: 𝔹 unit: Unit it: btrue: tt ifthenelse: if then else fi  cons: [a b] bfalse: ff exists: x:A. B[x] sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b false: False cand: c∧ B squash: T not: ¬A
Lemmas referenced :  list_induction list_wf l_member_wf bool_wf iseg_wf filter_wf5 subtype_rel_dep_function subtype_rel_sets_simple iseg_member filter_nil_lemma istype-void nil_wf filter_cons_lemma cons_wf istype-universe iseg_nil assert_of_null sqequal-nil nil_iseg cons_member eqtt_to_assert list-cases product_subtype_list eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot cons_iseg equal_wf assert_elim bfalse_wf bnot_wf btrue_neq_bfalse not_assert_elim
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  Error :lambdaFormation_alt,  cut thin introduction extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality sqequalRule Error :lambdaEquality_alt,  functionEquality hypothesis setEquality applyEquality Error :setIsType,  Error :universeIsType,  because_Cache independent_isectElimination dependent_functionElimination independent_functionElimination Error :isect_memberEquality_alt,  voidElimination Error :functionIsType,  rename Error :inhabitedIsType,  instantiate universeEquality productElimination equalityTransitivity equalitySymmetry Error :inlFormation_alt,  Error :dependent_set_memberEquality_alt,  unionElimination equalityElimination Error :inrFormation_alt,  Error :equalityIstype,  promote_hyp hypothesis_subsumption Error :dependent_pairFormation_alt,  cumulativity hyp_replacement applyLambdaEquality independent_pairFormation setElimination imageMemberEquality baseClosed imageElimination Error :productIsType

Latex:
\mforall{}[T:Type].  \mforall{}L2,L1:T  List.  \mforall{}P:\{x:T|  (x  \mmember{}  L2)\}    {}\mrightarrow{}  \mBbbB{}.    (L1  \mleq{}  L2  {}\mRightarrow{}  filter(P;L1)  \mleq{}  filter(P;L2))



Date html generated: 2019_06_20-PM-01_29_10
Last ObjectModification: 2019_01_17-PM-04_24_47

Theory : list_1


Home Index