Step
*
2
of Lemma
member-fset-mapfilter
1. T : Type
2. eqT : EqDecider(T)
3. P : T ⟶ 𝔹
4. X : Type
5. eqX : EqDecider(X)
6. f : {x:T| ↑(P x)} ⟶ X
7. s : fset(T)
8. x : X
9. ↓∃y:T. (y ∈ s ∧ (↑(P y)) ∧ (x = (f y) ∈ X))
⊢ x ∈ fset-mapfilter(f;P;s)
BY
{ ((SupposeNot THEN Assert ⌜0 = 1 ∈ ℤ⌝⋅ THEN Auto) THEN SqExRepD) }
1
1. T : Type
2. eqT : EqDecider(T)
3. P : T ⟶ 𝔹
4. X : Type
5. eqX : EqDecider(X)
6. f : {x:T| ↑(P x)} ⟶ X
7. s : fset(T)
8. x : X
9. y : T
10. y ∈ s
11. ↑(P y)
12. x = (f y) ∈ X
13. ¬x ∈ fset-mapfilter(f;P;s)
⊢ 0 = 1 ∈ ℤ
Latex:
Latex:
1. T : Type
2. eqT : EqDecider(T)
3. P : T {}\mrightarrow{} \mBbbB{}
4. X : Type
5. eqX : EqDecider(X)
6. f : \{x:T| \muparrow{}(P x)\} {}\mrightarrow{} X
7. s : fset(T)
8. x : X
9. \mdownarrow{}\mexists{}y:T. (y \mmember{} s \mwedge{} (\muparrow{}(P y)) \mwedge{} (x = (f y)))
\mvdash{} x \mmember{} fset-mapfilter(f;P;s)
By
Latex:
((SupposeNot THEN Assert \mkleeneopen{}0 = 1\mkleeneclose{}\mcdot{} THEN Auto) THEN SqExRepD)
Home
Index