---

Step * 2 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)
⊢ ↑((∀br(:|s|) ∈ ps. (¬b(r (=b) p))) ∧b distinct{s}(ps)) ⇐⇒ ∀x:|s|. ((b2i(p (=b) x) + (x #∈ ps)) ≤ 1)
BY
{ (RewriteWith []    ``ball_char assert_of_band assert_of_bnot assert_of_dset_eq`` 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 ∈b ps)) ⇒ (¬(r = p ∈ |s|)))) ∧ (↑distinct{s}(ps)) ⇐⇒ ∀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{}  \muparrow{}((\mforall{}\msubb{}r(:|s|)  \mmember{}  ps.  (\mneg{}\msubb{}(r  (=\msubb{})  p)))  \mwedge{}\msubb{}  distinct\{s\}(ps))
\mLeftarrow{}{}\mRightarrow{}  \mforall{}x:|s|.  ((b2i(p  (=\msubb{})  x)  +  (x  \#\mmember{}  ps))  \mleq{}  1)


By

---

Latex:
(RewriteWith  []        ``ball\_char  assert\_of\_band  assert\_of\_bnot  assert\_of\_dset\_eq``  0  THENA  Auto)

---

Home Index