---

Step * of Lemma mkpadic-equiv

∀[p:{2...}]. ∀[n:ℕ]. ∀[a:p-adics(p)].  ((a/p^n) ∈ {x:basic-padic(p)| bpa-equiv(p;<n, a>;x)} )
BY
{ (Auto THEN MemTypeCD THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[p:\{2...\}].  \mforall{}[n:\mBbbN{}].  \mforall{}[a:p-adics(p)].    ((a/p\^{}n)  \mmember{}  \{x:basic-padic(p)|  bpa-equiv(p;<n,  a>x)\}  )


By

---

Latex:
(Auto  THEN  MemTypeCD  THEN  Auto)

---

Home Index