---

Step * 1 of Lemma filter-fset-minimals


1. T : Type
2. eq : EqDecider(T)
3. less : T ⟶ T ⟶ 𝔹
4. s : fset(T)
5. P : T ⟶ 𝔹
6. ∀a,y:T.  ((↑P[a]) ⇒ (↑less[y;a]) ⇒ (↑P[y]))
7. a : T
8. a ∈ s
9. ↑P[a]
10. fset-all({a ∈ s | P[a]};y.¬bless[y;a])
11. a ∈ s
⊢ fset-all(s;y.¬bless[y;a])
BY
{ OnMaybeHyp 9 (\h. ((InstLemma `fset-all-iff` [⌜T⌝;⌜eq⌝]⋅ THENA Auto)
                     THEN (RWO "-1" h THENA Auto)
                     THEN (RWO "-1" 0 THENA Auto)
                     THEN ParallelOp h
                     THEN Auto
                     THEN (D 0 THENA Auto)
                     THEN D -3
                     THEN Auto
                     THEN RWO "member-fset-filter" 0
                     THEN Auto
                     THEN D 0
                     THEN Auto)) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  less  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}
4.  s  :  fset(T)
5.  P  :  T  {}\mrightarrow{}  \mBbbB{}
6.  \mforall{}a,y:T.    ((\muparrow{}P[a])  {}\mRightarrow{}  (\muparrow{}less[y;a])  {}\mRightarrow{}  (\muparrow{}P[y]))
7.  a  :  T
8.  a  \mmember{}  s
9.  \muparrow{}P[a]
10.  fset-all(\{a  \mmember{}  s  |  P[a]\};y.\mneg{}\msubb{}less[y;a])
11.  a  \mmember{}  s
\mvdash{}  fset-all(s;y.\mneg{}\msubb{}less[y;a])


By

---

Latex:
OnMaybeHyp  9  (\mbackslash{}h.  ((InstLemma  `fset-all-iff`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{}]\mcdot{}  THENA  Auto)
                                      THEN  (RWO  "-1"  h  THENA  Auto)
                                      THEN  (RWO  "-1"  0  THENA  Auto)
                                      THEN  ParallelOp  h
                                      THEN  Auto
                                      THEN  (D  0  THENA  Auto)
                                      THEN  D  -3
                                      THEN  Auto
                                      THEN  RWO  "member-fset-filter"  0
                                      THEN  Auto
                                      THEN  D  0
                                      THEN  Auto))

---

Home Index