Step
*
of Lemma
bexists_iff_exists_nth
∀s:DSet. ∀f:|s| ⟶ 𝔹. ∀as:|s| List. (↑∃b x(:|s|) ∈ as. f[x]
⇐⇒ ∃n:ℕ||as||. (↑f[as[n]]))
BY
{ (UnivCD THENA Auto) }
1
1. s : DSet
2. f : |s| ⟶ 𝔹
3. as : |s| List
⊢ ↑∃b x(:|s|) ∈ as. f[x]
⇐⇒ ∃n:ℕ||as||. (↑f[as[n]])
Latex:
Latex:
\mforall{}s:DSet. \mforall{}f:|s| {}\mrightarrow{} \mBbbB{}. \mforall{}as:|s| List. (\muparrow{}\mexists{}b x(:|s|) \mmember{} as. f[x] \mLeftarrow{}{}\mRightarrow{} \mexists{}n:\mBbbN{}||as||. (\muparrow{}f[as[n]]))
By
Latex:
(UnivCD THENA Auto)
Home
Index