Step
*
of Lemma
cont-induction-factorial
∀n:ℕ. (∃x:{ℤ| ((n)! = x ∈ ℤ)})
BY
{ (InstLemma `cont-induction-ext` [⌜λ2n.∃x:{ℤ| ((n)! = x ∈ ℤ)}⌝]⋅ THEN Auto) }
Latex:
Latex:
\mforall{}n:\mBbbN{}. (\mexists{}x:\{\mBbbZ{}| ((n)! = x)\})
By
Latex:
(InstLemma `cont-induction-ext` [\mkleeneopen{}\mlambda{}\msubtwo{}n.\mexists{}x:\{\mBbbZ{}| ((n)! = x)\}\mkleeneclose{}]\mcdot{} THEN Auto)
Home
Index