---

Step * of Lemma fset-find_wf

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[P:T ⟶ 𝔹]. ∀[s:fset(T)].
  (fset-find(P;s) ∈ {x:T| x ∈ s ∧ (↑(P x))} ) supposing 
     ((∀x,y:T.  (x ∈ s ⇒ y ∈ s ⇒ (↑(P x)) ⇒ (↑(P y)) ⇒ (x = y ∈ T))) and 
     (↓∃x:T. (x ∈ s ∧ (↑(P x)))))
BY
{ Auto }

1
1. T : Type
2. eq : EqDecider(T)
3. P : T ⟶ 𝔹
4. s : fset(T)
5. ∃x:T. (x ∈ s ∧ (↑(P x)))
6. ∀x,y:T.  (x ∈ s ⇒ y ∈ s ⇒ (↑(P x)) ⇒ (↑(P y)) ⇒ (x = y ∈ T))
⊢ fset-find(P;s) ∈ {x:T| x ∈ s ∧ (↑(P x))} 

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[s:fset(T)].
    (fset-find(P;s)  \mmember{}  \{x:T|  x  \mmember{}  s  \mwedge{}  (\muparrow{}(P  x))\}  )  supposing 
          ((\mforall{}x,y:T.    (x  \mmember{}  s  {}\mRightarrow{}  y  \mmember{}  s  {}\mRightarrow{}  (\muparrow{}(P  x))  {}\mRightarrow{}  (\muparrow{}(P  y))  {}\mRightarrow{}  (x  =  y)))  and 
          (\mdownarrow{}\mexists{}x:T.  (x  \mmember{}  s  \mwedge{}  (\muparrow{}(P  x)))))


By

---

Latex:
Auto

---

Home Index