---

Step * of Lemma fset-size-one

∀[T:Type]. ∀eq:EqDecider(T). ∀s:fset(T).  (||s|| = 1 ∈ ℤ ⇐⇒ ∃x:T. (x ∈ s ∧ (∀y:T. y = x ∈ T supposing y ∈ s)))
BY
{ TACTIC:Auto }

1
1. [T] : Type
2. eq : EqDecider(T)
3. s : fset(T)
4. ||s|| = 1 ∈ ℤ
⊢ ∃x:T. (x ∈ s ∧ (∀y:T. y = x ∈ T supposing y ∈ s))

2
1. T : Type
2. eq : EqDecider(T)
3. s : fset(T)
4. ∃x:T. (x ∈ s ∧ (∀y:T. y = x ∈ T supposing y ∈ s))
⊢ ||s|| = 1 ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}eq:EqDecider(T).  \mforall{}s:fset(T).    (||s||  =  1  \mLeftarrow{}{}\mRightarrow{}  \mexists{}x:T.  (x  \mmember{}  s  \mwedge{}  (\mforall{}y:T.  y  =  x  supposing  y  \mmember{}  s)))


By

---

Latex:
TACTIC:Auto

---

Home Index