Step
*
of Lemma
mset_mem_fmap
∀s,s':DSet. ∀f:|s| ⟶ |s'|. ∀x:|s|. ∀a:MSet{s}. ((↑(x ∈b a))
⇒ (↑((f x) ∈b fs-map(f, a))))
BY
{ ((RepD THENM Unfold `fset_map` 0) THENA Auto) }
1
1. s : DSet@i'
2. s' : DSet@i'
3. f : |s| ⟶ |s'|@i
4. x : |s|@i
5. a : MSet{s}@i
6. ↑(x
∈b a)@i
⊢ ↑((f x)
∈b fset_of_mset(s';msmap{s,s'}(f;a)))
Latex:
Latex:
\mforall{}s,s':DSet. \mforall{}f:|s| {}\mrightarrow{} |s'|. \mforall{}x:|s|. \mforall{}a:MSet\{s\}. ((\muparrow{}(x \mmember{}\msubb{} a)) {}\mRightarrow{} (\muparrow{}((f x) \mmember{}\msubb{} fs-map(f, a))))
By
Latex:
((RepD THENM Unfold `fset\_map` 0) THENA Auto)
Home
Index