---

Step * of Lemma rleq_antisymmetry

∀[x,y:ℝ].  (x = y) supposing ((y ≤ x) and (x ≤ y))
BY
{ (Auto THEN (All (RWO "rleq-iff4") THENA Auto) THEN D 0 THEN Auto THEN ∀h:hyp. (InstHyp [⌜n⌝] h⋅ THENA Auto) ) }

1
1. x : ℝ
2. y : ℝ
3. ∀n:ℕ+. ((x n) ≤ ((y n) + 4))
4. ∀n:ℕ+. ((y n) ≤ ((x n) + 4))
5. n : ℕ+
6. (y n) ≤ ((x n) + 4)
7. (x n) ≤ ((y n) + 4)
⊢ |(x n) - y n| ≤ 4

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbR{}].    (x  =  y)  supposing  ((y  \mleq{}  x)  and  (x  \mleq{}  y))


By

---

Latex:
(Auto
  THEN  (All  (RWO  "rleq-iff4")  THENA  Auto)
  THEN  D  0
  THEN  Auto
  THEN  \mforall{}h:hyp.  (InstHyp  [\mkleeneopen{}n\mkleeneclose{}]  h\mcdot{}  THENA  Auto)  )

---

Home Index