Step
*
1
1
of Lemma
bexists_char
1. s : DSet
2. f : |s| ⟶ 𝔹
⊢ False
⇐⇒ ∃x:|s|. (False ∧ (↑f[x]))
BY
{ (GenExRepD THEN Auto) }
Latex:
Latex:
1. s : DSet
2. f : |s| {}\mrightarrow{} \mBbbB{}
\mvdash{} False \mLeftarrow{}{}\mRightarrow{} \mexists{}x:|s|. (False \mwedge{} (\muparrow{}f[x]))
By
Latex:
(GenExRepD THEN Auto)
Home
Index