Step * of Lemma bmsexists_char_a

s:DSet. ∀f:|s| ⟶ 𝔹. ∀a:MSet{s}.  ((↑(∃b{s} x ∈ a. f[x]))  (↓∃x:|s|. ((↑(x ∈b a)) ∧ (↑f[x]))))
BY
((CDToVarThen `a' (\i. 
  CSquash THENM UseEqWitness Ax 
  THENM msetD THENM EqTypeCD) THENA Auto) }

1
1. DSet
2. |s| ⟶ 𝔹
3. as |s| List
4. bs |s| List
5. as ≡(|s|) bs
⊢ (↑(∃b{s} x ∈ as. f[x]))  (↓∃x:|s|. ((↑(x ∈b as)) ∧ (↑f[x])))


Latex:


Latex:
\mforall{}s:DSet.  \mforall{}f:|s|  {}\mrightarrow{}  \mBbbB{}.  \mforall{}a:MSet\{s\}.    ((\muparrow{}(\mexists{}\msubb{}\{s\}  x  \mmember{}  a.  f[x]))  {}\mRightarrow{}  (\mdownarrow{}\mexists{}x:|s|.  ((\muparrow{}(x  \mmember{}\msubb{}  a))  \mwedge{}  (\muparrow{}f[x]))))


By


Latex:
((CDToVarThen  `a'  (\mbackslash{}i. 
    CSquash  THENM  UseEqWitness  Ax 
    THENM  msetD  i  THENM  EqTypeCD)  )  THENA  Auto)




Home Index