---

Step * 1 1 of Lemma sublist_filter_2


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))
BY
{ TACTIC:(Assert filter(P;L1) ∈ T List BY
                (SubsumeC ⌜{x:T| (x ∈ L1)}  List⌝⋅ THEN Auto)) }

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)))
6. filter(P;L1) ∈ T List
⊢ 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{}
5.  \mforall{}L2:\{x:T|  (x  \mmember{}  L1)\}    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)))
\mvdash{}  L2  \msubseteq{}  filter(P;L1)  \mLeftarrow{}{}\mRightarrow{}  L2  \msubseteq{}  L1  \mwedge{}  (\mforall{}x\mmember{}L2.\muparrow{}(P  x))


By

---

Latex:
TACTIC:(Assert  filter(P;L1)  \mmember{}  T  List  BY
                            (SubsumeC  \mkleeneopen{}\{x:T|  (x  \mmember{}  L1)\}    List\mkleeneclose{}\mcdot{}  THEN  Auto))

---

Home Index