---

Step * 1 2 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
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)))
BY
{ (InstHyp [⌜||x|| + 1⌝;⌜x⌝] (-1)⋅ THEN Auto) }

---

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
7.  \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\}
                =  \{\})))
\mvdash{}  \mneg{}(\{y  \mmember{}  fset-minimals(xs,ys.f-proper-subset-dec(eq;xs;ys);  s)  |  deq-f-subset(eq)  y  x\}  =  \{\})


By

---

Latex:
(InstHyp  [\mkleeneopen{}||x||  +  1\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)

---

Home Index