Step * of Lemma comparison-connex

[T:Type]. ∀cmp:comparison(T). Connex(T;x,y.0 ≤ (cmp y))
BY
(Auto THEN THEN Auto THEN THEN Unhide THEN Auto) }

1
1. Type
2. cmp T ⟶ T ⟶ ℤ@i
3. ∀x,y:T.  ((cmp y) (-(cmp x)) ∈ ℤ)@i
4. ∀x,y:T.  (((cmp y) 0 ∈ ℤ (∀z:T. ((cmp z) (cmp z) ∈ ℤ)))@i
5. ∀x,y,z:T.  ((0 ≤ (cmp y))  (0 ≤ (cmp z))  (0 ≤ (cmp z)))@i
6. T@i
7. T@i
⊢ (0 ≤ (cmp y)) ∨ (0 ≤ (cmp x))


Latex:


Latex:
\mforall{}[T:Type].  \mforall{}cmp:comparison(T).  Connex(T;x,y.0  \mleq{}  (cmp  x  y))


By


Latex:
(Auto  THEN  D  0  THEN  Auto  THEN  D  2  THEN  Unhide  THEN  Auto)




Home Index