---

Step * 1 of Lemma fset-closure-exists2

.....antecedent..... 
1. T : Type
2. eq : EqDecider(T)
3. r : T ⟶ ℕ
4. fs : {f:T ⟶ T| ∀x:T. r (f x) < r x supposing ¬((f x) = x ∈ T)}  List
5. s : fset(T)
⊢ (∀f∈fs.∀x:T. ((¬((f x) = x ∈ T)) ⇒ r (f x) < r x))
BY
{ ((BLemma `l_all_iff` THEN Auto) THEN RepeatFor 2 (D -3) THEN MoveToConcl (-1)) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  r  :  T  {}\mrightarrow{}  \mBbbN{}
4.  fs  :  \{f:T  {}\mrightarrow{}  T|  \mforall{}x:T.  r  (f  x)  <  r  x  supposing  \mneg{}((f  x)  =  x)\}    List
5.  s  :  fset(T)
\mvdash{}  (\mforall{}f\mmember{}fs.\mforall{}x:T.  ((\mneg{}((f  x)  =  x))  {}\mRightarrow{}  r  (f  x)  <  r  x))


By

---

Latex:
((BLemma  `l\_all\_iff`  THEN  Auto)  THEN  RepeatFor  2  (D  -3)  THEN  MoveToConcl  (-1))

---

Home Index