---

Step * 1 1 2 of Lemma bag-partitions-cons


1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. x : X
5. b : bag(X)
6. bag-no-repeats(bag(X) × bag(X);bag-partitions(eq;x.b))
7. ∀[f:(bag(X) × bag(X)) ⟶ (bag(X) × bag(X))]. ∀[bs:bag(bag(X) × bag(X))].
     uiff(bag-no-repeats(bag(X) × bag(X);bag-map(f;bs));bag-no-repeats(bag(X) × bag(X);bs)) 
     supposing Inj(bag(X) × bag(X);bag(X) × bag(X);f)
⊢ bag-no-repeats(bag(X) × bag(X);[p∈bag-partitions(eq;b)|((#x in snd(p)) =z 0)])
BY
{ ((BLemma `bag-filter-no-repeats` THEN Auto) THEN BLemma `no-repeats-bag-partitions` THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  Type
2.  valueall-type(X)
3.  eq  :  EqDecider(X)
4.  x  :  X
5.  b  :  bag(X)
6.  bag-no-repeats(bag(X)  \mtimes{}  bag(X);bag-partitions(eq;x.b))
7.  \mforall{}[f:(bag(X)  \mtimes{}  bag(X))  {}\mrightarrow{}  (bag(X)  \mtimes{}  bag(X))].  \mforall{}[bs:bag(bag(X)  \mtimes{}  bag(X))].
          uiff(bag-no-repeats(bag(X)  \mtimes{}  bag(X);bag-map(f;bs));bag-no-repeats(bag(X)  \mtimes{}  bag(X);bs)) 
          supposing  Inj(bag(X)  \mtimes{}  bag(X);bag(X)  \mtimes{}  bag(X);f)
\mvdash{}  bag-no-repeats(bag(X)  \mtimes{}  bag(X);[p\mmember{}bag-partitions(eq;b)|((\#x  in  snd(p))  =\msubz{}  0)])


By

---

Latex:
((BLemma  `bag-filter-no-repeats`  THEN  Auto)  THEN  BLemma  `no-repeats-bag-partitions`  THEN  Auto)

---

Home Index