---

Step * of Lemma equal-padics

∀[p:ℤ]. ∀[x,y:padic(p)].  uiff(x = y ∈ padic(p);x = y ∈ basic-padic(p))
BY
{ (Intros THEN (RepeatFor 2 (D 0) THENA Auto)) }

1
1. p : ℤ
2. x : padic(p)
3. y : padic(p)
4. x = y ∈ padic(p)
⊢ x = y ∈ basic-padic(p)

2
1. p : ℤ
2. x : padic(p)
3. y : padic(p)
4. x = y ∈ basic-padic(p)
⊢ x = y ∈ padic(p)

---

Latex:

---

Latex:
\mforall{}[p:\mBbbZ{}].  \mforall{}[x,y:padic(p)].    uiff(x  =  y;x  =  y)


By

---

Latex:
(Intros  THEN  (RepeatFor  2  (D  0)  THENA  Auto))

---

Home Index