---

Step * 1 of Lemma sublist_filter_2


1. [T] : Type
2. L1 : T List
3. L2 : T List
4. P : {x:T| (x ∈ L1)}  ⟶ 𝔹
⊢ L2 ⊆ filter(P;L1) ⇐⇒ L2 ⊆ L1 ∧ (∀x∈L2.↑(P x))
BY
{ ((InstLemma `sublist_filter` [⌜{x:T| (x ∈ L1)} ⌝]⋅ THENA Auto)
   THEN (InstHyp [⌜L1⌝] (-1)⋅ THENA BLemma `list-subtype` THENA Auto)
   THEN Thin (-2)) }

1
1. [T] : Type
2. L1 : T List
3. L2 : T List
4. P : {x:T| (x ∈ L1)}  ⟶ 𝔹
5. ∀L2:{x:T| (x ∈ L1)}  List. ∀P:{x:T| (x ∈ L1)}  ⟶ 𝔹.  (L2 ⊆ filter(P;L1) ⇐⇒ L2 ⊆ L1 ∧ (∀x∈L2.↑(P x)))
⊢ L2 ⊆ filter(P;L1) ⇐⇒ L2 ⊆ L1 ∧ (∀x∈L2.↑(P x))

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  L1  :  T  List
3.  L2  :  T  List
4.  P  :  \{x:T|  (x  \mmember{}  L1)\}    {}\mrightarrow{}  \mBbbB{}
\mvdash{}  L2  \msubseteq{}  filter(P;L1)  \mLeftarrow{}{}\mRightarrow{}  L2  \msubseteq{}  L1  \mwedge{}  (\mforall{}x\mmember{}L2.\muparrow{}(P  x))


By

---

Latex:
((InstLemma  `sublist\_filter`  [\mkleeneopen{}\{x:T|  (x  \mmember{}  L1)\}  \mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}L1\mkleeneclose{}]  (-1)\mcdot{}  THENA  BLemma  `list-subtype`  THENA  Auto)
  THEN  Thin  (-2))

---

Home Index