---

Step * 1 of Lemma no-repeats-iff-count


1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. no_repeats(T;L)
5. x : T
6. 1 ≤ ||filter(eq x;L)||
⊢ ||filter(eq x;L)|| = 1 ∈ ℤ
BY
{ ((InstLemma `set-equal-no_repeats-length` [⌜T⌝;⌜[filter(eq x;L)[0]]⌝;⌜filter(eq x;L)⌝]⋅ THENA Auto)
   THEN Reduce (-1)
   THEN Auto) }

1
.....antecedent..... 
1. T : Type
2. eq : EqDecider(T)
3. L : T List
4. no_repeats(T;L)
5. x : T
6. 1 ≤ ||filter(eq x;L)||
⊢ set-equal(T;[filter(eq x;L)[0]];filter(eq x;L))

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  L  :  T  List
4.  no\_repeats(T;L)
5.  x  :  T
6.  1  \mleq{}  ||filter(eq  x;L)||
\mvdash{}  ||filter(eq  x;L)||  =  1


By

---

Latex:
((InstLemma  `set-equal-no\_repeats-length`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}[filter(eq  x;L)[0]]\mkleeneclose{};\mkleeneopen{}filter(eq  x;L)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  Auto)

---

Home Index