### Nuprl Lemma : sublist_filter_2

`∀[T:Type]. ∀L1,L2:T List. ∀P:{x:T| (x ∈ L1)}  ⟶ 𝔹.  (L2 ⊆ filter(P;L1) `⇐⇒` L2 ⊆ L1 ∧ (∀x∈L2.↑(P x)))`

Proof

Definitions occuring in Statement :  sublist: `L1 ⊆ L2` l_all: `(∀x∈L.P[x])` l_member: `(x ∈ l)` filter: `filter(P;l)` list: `T List` assert: `↑b` bool: `𝔹` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` set: `{x:A| B[x]} ` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` member: `t ∈ T` prop: `ℙ` subtype_rel: `A ⊆r B` uimplies: `b supposing a` iff: `P `⇐⇒` Q` and: `P ∧ Q` implies: `P `` Q` rev_implies: `P `` Q` guard: `{T}` so_lambda: `λ2x.t[x]` so_apply: `x[s]` sublist: `L1 ⊆ L2` exists: `∃x:A. B[x]` int_seg: `{i..j-}` lelt: `i ≤ j < k` decidable: `Dec(P)` or: `P ∨ Q` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` false: `False` top: `Top` less_than: `a < b` squash: `↓T` ge: `i ≥ j ` nat: `ℕ` cand: `A c∧ B` true: `True`
Lemmas referenced :  l_member_wf bool_wf list_wf sublist_filter list-subtype filter_wf2 subtype_rel_list member_sublist member_filter_2 subtype_rel_list_set increasing_wf length_wf_nat int_seg_wf length_wf select_wf int_seg_properties decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf decidable__lt intformless_wf int_formula_prop_less_lemma non_neg_length le_wf less_than_wf nat_properties select_member equal_wf sublist_wf squash_wf true_wf subtype_rel_self iff_weakening_equal l_all_wf assert_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  Error :lambdaFormation_alt,  Error :functionIsType,  Error :setIsType,  Error :universeIsType,  hypothesisEquality cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesis Error :inhabitedIsType,  universeEquality setEquality dependent_functionElimination applyEquality independent_isectElimination Error :lambdaEquality_alt,  setElimination rename sqequalRule independent_pairFormation equalityTransitivity equalitySymmetry independent_functionElimination productElimination because_Cache Error :dependent_pairFormation_alt,  Error :productIsType,  functionExtensionality natural_numberEquality Error :equalityIsType1,  unionElimination approximateComputation int_eqEquality Error :isect_memberEquality_alt,  voidElimination imageElimination Error :dependent_set_memberEquality_alt,  applyLambdaEquality promote_hyp hyp_replacement imageMemberEquality baseClosed instantiate

Latex:
\mforall{}[T:Type].  \mforall{}L1,L2:T  List.  \mforall{}P:\{x:T|  (x  \mmember{}  L1)\}    {}\mrightarrow{}  \mBbbB{}.    (L2  \msubseteq{}  filter(P;L1)  \mLeftarrow{}{}\mRightarrow{}  L2  \msubseteq{}  L1  \mwedge{}  (\mforall{}x\mmember{}L2.\muparrow{}(P  x))\000C)

Date html generated: 2019_06_20-PM-01_26_25
Last ObjectModification: 2018_10_15-PM-05_47_45

Theory : list_1

Home Index