---

Step * of Lemma b_all-map

∀[A,B:Type].
  ∀f:A ⟶ B. ∀b:bag(A). ∀P:B ⟶ ℙ.  ((∀b:B. SqStable(P[b])) ⇒ (b_all(B;bag-map(f;b);x.P[x]) ⇐⇒ b_all(A;b;x.P[f x])))
BY
{ ((UnivCD THENA Auto) THEN RepUR ``b_all`` 0 THEN RWO "bag-member-map" 0 THEN Auto) }

1
1. [A] : Type
2. [B] : Type
3. f : A ⟶ B
4. b : bag(A)
5. P : B ⟶ ℙ
6. ∀b:B. SqStable(P[b])
7. ∀x:A. (x ↓∈ b ⇒ P[f x])
8. x : B
9. ↓∃v:A. (v ↓∈ b ∧ (x = (f v) ∈ B))
⊢ P[x]

---

Latex:

---

Latex:
\mforall{}[A,B:Type].
    \mforall{}f:A  {}\mrightarrow{}  B.  \mforall{}b:bag(A).  \mforall{}P:B  {}\mrightarrow{}  \mBbbP{}.
        ((\mforall{}b:B.  SqStable(P[b]))  {}\mRightarrow{}  (b\_all(B;bag-map(f;b);x.P[x])  \mLeftarrow{}{}\mRightarrow{}  b\_all(A;b;x.P[f  x])))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RepUR  ``b\_all``  0  THEN  RWO  "bag-member-map"  0  THEN  Auto)

---

Home Index