---

Step * of Lemma equal-p-adics

∀[p:ℕ+]. ∀[x,y:p-adics(p)].  uiff(x = y ∈ p-adics(p);x = y ∈ (ℕ+ ⟶ ℤ))
BY
{ (Intro
   THEN (Assert p-adics(p) ⊆r (ℕ+ ⟶ ℤ) BY
               Auto)
   THEN Intros
   THEN (RepeatFor 2 (D 0) THENA Auto)
   THEN DVar `x'
   THEN DVar `y'
   THEN ((EqTypeHD (-1) THEN Auto) ORELSE (EqTypeCD THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[p:\mBbbN{}\msupplus{}].  \mforall{}[x,y:p-adics(p)].    uiff(x  =  y;x  =  y)


By

---

Latex:
(Intro
  THEN  (Assert  p-adics(p)  \msubseteq{}r  (\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{})  BY
                          Auto)
  THEN  Intros
  THEN  (RepeatFor  2  (D  0)  THENA  Auto)
  THEN  DVar  `x'
  THEN  DVar  `y'
  THEN  ((EqTypeHD  (-1)  THEN  Auto)  ORELSE  (EqTypeCD  THEN  Auto)))

---

Home Index