Step
*
of Lemma
mset_for_when_unique
∀s:DSet. ∀g:IAbMonoid. ∀f:|s| ⟶ |g|. ∀b:|s| ⟶ 𝔹. ∀u:|s|.
((↑b[u])
⇒ (∀as:MSet{s}
((∀x:|s|. ((x #∈ as) ≤ 1))
⇒ (↑(u
∈b as))
⇒ (∀v:|s|. ((↑b[v])
⇒ (↑(v ∈b as))
⇒ (v = u ∈ |s|)))
⇒ ((msFor{g} x ∈ as. when b[x]. f[x]) = f[u] ∈ |g|))))
BY
{ ((CDToVarThen `as' (\i.CSquash)) THENA Auto) }
1
1. s : DSet
2. g : IAbMonoid
3. f : |s| ⟶ |g|
4. b : |s| ⟶ 𝔹
5. u : |s|
6. ↑b[u]
7. as : MSet{s}
⊢ ↓(∀x:|s|. ((x #∈ as) ≤ 1))
⇒ (↑(u
∈b as))
⇒ (∀v:|s|. ((↑b[v])
⇒ (↑(v ∈b as))
⇒ (v = u ∈ |s|)))
⇒ ((msFor{g} x ∈ as. when b[x]. f[x]) = f[u] ∈ |g|)
Latex:
Latex:
\mforall{}s:DSet. \mforall{}g:IAbMonoid. \mforall{}f:|s| {}\mrightarrow{} |g|. \mforall{}b:|s| {}\mrightarrow{} \mBbbB{}. \mforall{}u:|s|.
((\muparrow{}b[u])
{}\mRightarrow{} (\mforall{}as:MSet\{s\}
((\mforall{}x:|s|. ((x \#\mmember{} as) \mleq{} 1))
{}\mRightarrow{} (\muparrow{}(u
\mmember{}\msubb{} as))
{}\mRightarrow{} (\mforall{}v:|s|. ((\muparrow{}b[v]) {}\mRightarrow{} (\muparrow{}(v \mmember{}\msubb{} as)) {}\mRightarrow{} (v = u)))
{}\mRightarrow{} ((msFor\{g\} x \mmember{} as. when b[x]. f[x]) = f[u]))))
By
Latex:
((CDToVarThen `as' (\mbackslash{}i.CSquash)) THENA Auto)
Home
Index