Step * of Lemma list-is-singleton-iff

No Annotations
[T:Type]. ∀L:T List. ∀x:T.  (L [x] ∈ (T List) ⇐⇒ no_repeats(T;L) ∧ (∀f:T. ((f ∈ L) ⇐⇒ x ∈ T)))
BY
Auto }

1
1. Type
2. List
3. T
4. [x] ∈ (T List)
⊢ no_repeats(T;L)

2
1. Type
2. List
3. T
4. [x] ∈ (T List)
5. T
6. (f ∈ L)
⊢ x ∈ T

3
1. [T] Type
2. List
3. T
4. [x] ∈ (T List)
5. T
6. x ∈ T
⊢ (f ∈ L)

4
1. Type
2. List
3. T
4. no_repeats(T;L)
5. ∀f:T. ((f ∈ L) ⇐⇒ x ∈ T)
⊢ [x] ∈ (T List)


Latex:


Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}L:T  List.  \mforall{}x:T.    (L  =  [x]  \mLeftarrow{}{}\mRightarrow{}  no\_repeats(T;L)  \mwedge{}  (\mforall{}f:T.  ((f  \mmember{}  L)  \mLeftarrow{}{}\mRightarrow{}  f  =  x)))


By


Latex:
Auto




Home Index