---

Step * of Lemma least-upper-bound-assoc

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  ∀[a,b,c,x,y,u1,u2:T].
    (u1 = u2 ∈ T) supposing 
       (least-upper-bound(T;x,y.R[x;y];a;b;x) and 
       least-upper-bound(T;x,y.R[x;y];x;c;u1) and 
       least-upper-bound(T;x,y.R[x;y];b;c;y) and 
       least-upper-bound(T;x,y.R[x;y];a;y;u2)) 
  supposing Order(T;x,y.R[x;y])
BY
{ Auto }

1
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. Order(T;x,y.R[x;y])
4. a : T
5. b : T
6. c : T
7. x : T
8. y : T
9. u1 : T
10. u2 : T
11. least-upper-bound(T;x,y.R[x;y];a;y;u2)
12. least-upper-bound(T;x,y.R[x;y];b;c;y)
13. least-upper-bound(T;x,y.R[x;y];x;c;u1)
14. least-upper-bound(T;x,y.R[x;y];a;b;x)
⊢ u1 = u2 ∈ T

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}[a,b,c,x,y,u1,u2:T].
        (u1  =  u2)  supposing 
              (least-upper-bound(T;x,y.R[x;y];a;b;x)  and 
              least-upper-bound(T;x,y.R[x;y];x;c;u1)  and 
              least-upper-bound(T;x,y.R[x;y];b;c;y)  and 
              least-upper-bound(T;x,y.R[x;y];a;y;u2)) 
    supposing  Order(T;x,y.R[x;y])


By

---

Latex:
Auto

---

Home Index