---

Step * of Lemma ni-eventually-equal-equiv

No Annotations
EquivRel(ℕ∞;f,g.ni-eventually-equal(f;g))
BY
{ (RepUR ``equiv_rel refl sym trans`` 0 THEN Auto THEN All (Unfold `ni-eventually-equal`)⋅) }

1
1. a : ℕ∞
⊢ ∃n:ℕ. ∀m:{n...}. a m = a m

2
1. ∀a:ℕ∞. ∃n:ℕ. ∀m:{n...}. a m = a m
2. a : ℕ∞
3. b : ℕ∞
4. ∃n:ℕ. ∀m:{n...}. a m = b m
⊢ ∃n:ℕ. ∀m:{n...}. b m = a m

3
1. ∀a:ℕ∞. ∃n:ℕ. ∀m:{n...}. a m = a m
2. ∀a,b:ℕ∞.  ((∃n:ℕ. ∀m:{n...}. a m = b m) ⇒ (∃n:ℕ. ∀m:{n...}. b m = a m))
3. a : ℕ∞
4. b : ℕ∞
5. c : ℕ∞
6. ∃n:ℕ. ∀m:{n...}. a m = b m
7. ∃n:ℕ. ∀m:{n...}. b m = c m
⊢ ∃n:ℕ. ∀m:{n...}. a m = c m

---

Latex:

---

Latex:
No  Annotations
EquivRel(\mBbbN{}\minfty{};f,g.ni-eventually-equal(f;g))


By

---

Latex:
(RepUR  ``equiv\_rel  refl  sym  trans``  0  THEN  Auto  THEN  All  (Unfold  `ni-eventually-equal`)\mcdot{})

---

Home Index