---

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

.....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)))))
BY
{ (RepeatFor 2 (Thin (-1)) THEN InductionOnNat THEN Auto') }

1
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. n : ℤ
6. 0 < n
7. ∀x:fset(T)
     (||x|| < n - 1
     ⇒ x ∈ s
     ⇒ (¬({y ∈ fset-minimals(xs,ys.f-proper-subset-dec(eq;xs;ys); s) | deq-f-subset(eq) y x} = {} ∈ fset(fset(T)))))
8. x : fset(T)
9. ||x|| < n
10. x ∈ s
⊢ ¬({y ∈ fset-minimals(xs,ys.f-proper-subset-dec(eq;xs;ys); s) | deq-f-subset(eq) y x} = {} ∈ fset(fset(T)))

---

Latex:

---

Latex:
.....assertion..... 
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{}  \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\}  =  \{\})))


By

---

Latex:
(RepeatFor  2  (Thin  (-1))  THEN  InductionOnNat  THEN  Auto')

---

Home Index