Step * 2 1 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
10. y āˆˆ s
11. ā†‘(P y)
12. x = (f y) āˆˆ X
13. Ā¬x āˆˆ fset-mapfilter(f;P;s)
āŠ¢ 0 = 1 āˆˆ ā„¤
BY
{ (Dquotient2 7
   THEN D -1
   THEN Unfold `fset-mapfilter` 0
   THEN Unfold `fset-member` 0
   THEN RW assert_pushdownC 0
   THEN Auto
   THEN BLemma `member-mapfilter`
   THEN Auto) }

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. istype(T List)
8. āˆ€x1,y1:T List.  istype(set-equal(T;x1;y1))
9. āˆ€x1:T List. set-equal(T;x1;x1)
10. a : Base
11. b : Base
12. c : a = b āˆˆ pertype(Ī»x,y. ((x āˆˆ T List) āˆ§ (y āˆˆ T List) āˆ§ set-equal(T;x;y)))
13. a āˆˆ T List
14. b āˆˆ T List
15. set-equal(T;a;b)
16. x : X
17. y : T
18. y āˆˆ a
19. ā†‘(P y)
20. x = (f y) āˆˆ X
āŠ¢ āˆƒy:T. ((y āˆˆ a) āˆ§ ((ā†‘(P y)) cāˆ§ (x = (f y) āˆˆ X)))

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.  y  :  T
10.  y  \mmember{}  s
11.  \muparrow{}(P  y)
12.  x  =  (f  y)
13.  \mneg{}x  \mmember{}  fset-mapfilter(f;P;s)
\mvdash{}  0  =  1


By

Latex:
(Dquotient2  7
  THEN  D  -1
  THEN  Unfold  `fset-mapfilter`  0
  THEN  Unfold  `fset-member`  0
  THEN  RW  assert\_pushdownC  0
  THEN  Auto
  THEN  BLemma  `member-mapfilter`
  THEN  Auto)



Home Index