---

Step * 2 1 of Lemma distinct_iff_counts_le_one


1. s : DSet
2. p : |s|
3. ps : |s| List
4. ↑distinct{s}(ps) ⇐⇒ ∀x:|s|. ((x #∈ ps) ≤ 1)
⊢ (∀r:|s|. ((↑(r ∈b ps)) ⇒ (¬(r = p ∈ |s|)))) ∧ (↑distinct{s}(ps)) ⇐⇒ ∀x:|s|. ((b2i(p (=b) x) + (x #∈ ps)) ≤ 1)
BY
{ (RewriteWith [4] ``mem_iff_count_nzero`` 0 THENA Auto) }

1
1. s : DSet
2. p : |s|
3. ps : |s| List
4. ↑distinct{s}(ps) ⇐⇒ ∀x:|s|. ((x #∈ ps) ≤ 1)
⊢ (∀r:|s|. (((r #∈ ps) > 0) ⇒ (¬(r = p ∈ |s|)))) ∧ (∀x:|s|. ((x #∈ ps) ≤ 1))
⇐⇒ ∀x:|s|. ((b2i(p (=b) x) + (x #∈ ps)) ≤ 1)

---

Latex:

---

Latex:

1.  s  :  DSet
2.  p  :  |s|
3.  ps  :  |s|  List
4.  \muparrow{}distinct\{s\}(ps)  \mLeftarrow{}{}\mRightarrow{}  \mforall{}x:|s|.  ((x  \#\mmember{}  ps)  \mleq{}  1)
\mvdash{}  (\mforall{}r:|s|.  ((\muparrow{}(r  \mmember{}\msubb{}  ps))  {}\mRightarrow{}  (\mneg{}(r  =  p))))  \mwedge{}  (\muparrow{}distinct\{s\}(ps))
\mLeftarrow{}{}\mRightarrow{}  \mforall{}x:|s|.  ((b2i(p  (=\msubb{})  x)  +  (x  \#\mmember{}  ps))  \mleq{}  1)


By

---

Latex:
(RewriteWith  [4]  ``mem\_iff\_count\_nzero``  0  THENA  Auto)

---

Home Index