---

Step * of Lemma filter-fset-minimals

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[less:T ⟶ T ⟶ 𝔹]. ∀[s:fset(T)]. ∀[P:T ⟶ 𝔹].
  {a ∈ fset-minimals(x,y.less[x;y]; s) | P[a]} = fset-minimals(x,y.less[x;y]; {a ∈ s | P[a]}) ∈ fset(T) 
  supposing ∀a,y:T.  ((↑P[a]) ⇒ (↑less[y;a]) ⇒ (↑P[y]))
BY
{ ((UnivCD THENA Auto)
   THEN UsingVars [`eq'] (BLemma `fset-extensionality`)
   THEN Auto
   THEN RepeatFor 2 (((RWW  "member-fset-minimals member-fset-filter" (-1) THENA Auto)
                      THEN (RWW  "member-fset-minimals member-fset-filter" 0 THENA Auto)
                      THEN All (Unfold `guard`)⋅))
   THEN Auto
   THEN Try (OnMaybeHyp 8 (\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 ParallelLast
                                THEN RWO "member-fset-filter" (-1)
                                THEN Auto
                                THEN D -1
                                THEN Auto)))) }

1
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])

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[less:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[s:fset(T)].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].
    \{a  \mmember{}  fset-minimals(x,y.less[x;y];  s)  |  P[a]\}  =  fset-minimals(x,y.less[x;y];  \{a  \mmember{}  s  |  P[a]\}) 
    supposing  \mforall{}a,y:T.    ((\muparrow{}P[a])  {}\mRightarrow{}  (\muparrow{}less[y;a])  {}\mRightarrow{}  (\muparrow{}P[y]))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  UsingVars  [`eq']  (BLemma  `fset-extensionality`)
  THEN  Auto
  THEN  RepeatFor  2  (((RWW    "member-fset-minimals  member-fset-filter"  (-1)  THENA  Auto)
                                        THEN  (RWW    "member-fset-minimals  member-fset-filter"  0  THENA  Auto)
                                        THEN  All  (Unfold  `guard`)\mcdot{}))
  THEN  Auto
  THEN  Try  (OnMaybeHyp  8  (\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  ParallelLast
                                                            THEN  RWO  "member-fset-filter"  (-1)
                                                            THEN  Auto
                                                            THEN  D  -1
                                                            THEN  Auto))))

---

Home Index