---

Step * 1 of Lemma fset-minimals-ac-le


1. T : Type
2. eq : EqDecider(T)
3. s : fset(fset(T))
4. ∀[P:fset(T) ⟶ 𝔹]. ∀[s:fset(fset(T))].  uiff(fset-all(s;x.P[x]);∀[x:fset(T)]. ↑P[x] supposing x ∈ s)
5. x : fset(T)
6. x ∈ s
⊢ ¬({y ∈ fset-minimals(xs,ys.f-proper-subset-dec(eq;xs;ys); s) | deq-f-subset(eq) y x} = {} ∈ fset(fset(T)))
BY
{ Assert ⌜∀n:ℕ. ∀x:fset(T).
            (||x|| < n
            ⇒ x ∈ s
            ⇒ (¬({y ∈ fset-minimals(xs,ys.f-proper-subset-dec(eq;xs;ys); s) | deq-f-subset(eq) y x}
               = {}
               ∈ fset(fset(T)))))⌝⋅ }

1
.....assertion..... 
1. T : Type
2. eq : EqDecider(T)
3. s : fset(fset(T))
4. ∀[P:fset(T) ⟶ 𝔹]. ∀[s:fset(fset(T))].  uiff(fset-all(s;x.P[x]);∀[x:fset(T)]. ↑P[x] supposing x ∈ s)
5. x : fset(T)
6. x ∈ s
⊢ ∀n:ℕ. ∀x:fset(T).
    (||x|| < n
    ⇒ x ∈ s
    ⇒ (¬({y ∈ fset-minimals(xs,ys.f-proper-subset-dec(eq;xs;ys); s) | deq-f-subset(eq) y x} = {} ∈ fset(fset(T)))))

2
1. T : Type
2. eq : EqDecider(T)
3. s : fset(fset(T))
4. ∀[P:fset(T) ⟶ 𝔹]. ∀[s:fset(fset(T))].  uiff(fset-all(s;x.P[x]);∀[x:fset(T)]. ↑P[x] supposing x ∈ s)
5. x : fset(T)
6. x ∈ s
7. ∀n:ℕ. ∀x:fset(T).
     (||x|| < n
     ⇒ x ∈ s
     ⇒ (¬({y ∈ fset-minimals(xs,ys.f-proper-subset-dec(eq;xs;ys); s) | deq-f-subset(eq) y x} = {} ∈ fset(fset(T)))))
⊢ ¬({y ∈ fset-minimals(xs,ys.f-proper-subset-dec(eq;xs;ys); s) | deq-f-subset(eq) y x} = {} ∈ fset(fset(T)))

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  s  :  fset(fset(T))
4.  \mforall{}[P:fset(T)  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[s:fset(fset(T))].
          uiff(fset-all(s;x.P[x]);\mforall{}[x:fset(T)].  \muparrow{}P[x]  supposing  x  \mmember{}  s)
5.  x  :  fset(T)
6.  x  \mmember{}  s
\mvdash{}  \mneg{}(\{y  \mmember{}  fset-minimals(xs,ys.f-proper-subset-dec(eq;xs;ys);  s)  |  deq-f-subset(eq)  y  x\}  =  \{\})


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  \mforall{}x:fset(T).
                    (||x||  <  n
                    {}\mRightarrow{}  x  \mmember{}  s
                    {}\mRightarrow{}  (\mneg{}(\{y  \mmember{}  fset-minimals(xs,ys.f-proper-subset-dec(eq;xs;ys);  s)  |  deq-f-subset(eq)  y  x\}
                          =  \{\})))\mkleeneclose{}\mcdot{}

---

Home Index