Step
*
1
of Lemma
sublist_filter
1. [T] : Type
⊢ ∀P:T ⟶ 𝔹. ([] ⊆ [] ⇐⇒ [] ⊆ [] ∧ (∀x∈[].↑(P x)))
BY
{ Auto }
Latex:
Latex:
1. [T] : Type
\mvdash{} \mforall{}P:T {}\mrightarrow{} \mBbbB{}. ([] \msubseteq{} [] \mLeftarrow{}{}\mRightarrow{} [] \msubseteq{} [] \mwedge{} (\mforall{}x\mmember{}[].\muparrow{}(P x)))
By
Latex:
Auto
Home
Index