---

Step * of Lemma approx-per-for-mono

∀[T:Type]. ∀x,y:Base.  approx-per(T;x;y) supposing x = y ∈ T supposing mono(T)
BY
{ (Auto THEN ((D 0 THEN Auto) THENL [(D 0 With ⌜y⌝  THEN Auto); (D 0 With ⌜x⌝  THEN Auto)])) }

1
1. T : Type
2. mono(T)
3. x : Base
4. y : Base
5. x = y ∈ T
6. t : Base
7. x ≤ t
8. t ∈ T
9. y ≤ y
⊢ y = t ∈ T

2
1. T : Type
2. mono(T)
3. x : Base
4. y : Base
5. x = y ∈ T
6. ∀t:Base. (((x ≤ t) ∧ (t ∈ T)) ⇒ (∃t':Base. ((y ≤ t') ∧ (t' = t ∈ T))))
7. t : Base
8. y ≤ t
9. t ∈ T
10. x ≤ x
⊢ x = t ∈ T

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}x,y:Base.    approx-per(T;x;y)  supposing  x  =  y  supposing  mono(T)


By

---

Latex:
(Auto  THEN  ((D  0  THEN  Auto)  THENL  [(D  0  With  \mkleeneopen{}y\mkleeneclose{}    THEN  Auto);  (D  0  With  \mkleeneopen{}x\mkleeneclose{}    THEN  Auto)]))

---

Home Index