Step
*
of Lemma
s-filter_wf
∀[T:Type]. ∀[as:T List]. ∀[P:{a:T| (a ∈ as)} ⟶ 𝔹]. s-filter(P;as) ∈ T List supposing T ⊆r ℤ
BY
{ (((Auto THEN (InstLemma `list-subtype` [⌜T⌝; ⌜as⌝])⋅) THENA Auto) THEN Unfold `s-filter` 0 THEN Auto) }
Latex:
Latex:
\mforall{}[T:Type]. \mforall{}[as:T List]. \mforall{}[P:\{a:T| (a \mmember{} as)\} {}\mrightarrow{} \mBbbB{}]. s-filter(P;as) \mmember{} T List supposing T \msubseteq{}r \mBbbZ{}
By
Latex:
(((Auto THEN (InstLemma `list-subtype` [\mkleeneopen{}T\mkleeneclose{}; \mkleeneopen{}as\mkleeneclose{}])\mcdot{}) THENA Auto)
THEN Unfold `s-filter` 0
THEN Auto)
Home
Index