Step
*
1
1
1
1
1
1
of Lemma
ratio-functional-equation
1. [T] : Type
2. t : T
3. F : T ⟶ T ⟶ ℝ
4. ∀x,y,z:T. (((F x y) * (F y z)) = (F x z))
5. (F t t) = r1
6. x : T
7. ((F t x) * (F x t)) = r1
8. ((F t x) * (F x t)) = r1
⊢ F x t ≠ r0
BY
{ ((Assert r0 < ((F t x) * (F x t)) BY
(RWO "-1" 0 THEN Auto))
THEN (RWO "rmul-is-positive" (-1) THENM D -1)
THEN Auto) }
Latex:
Latex:
1. [T] : Type
2. t : T
3. F : T {}\mrightarrow{} T {}\mrightarrow{} \mBbbR{}
4. \mforall{}x,y,z:T. (((F x y) * (F y z)) = (F x z))
5. (F t t) = r1
6. x : T
7. ((F t x) * (F x t)) = r1
8. ((F t x) * (F x t)) = r1
\mvdash{} F x t \mneq{} r0
By
Latex:
((Assert r0 < ((F t x) * (F x t)) BY
(RWO "-1" 0 THEN Auto))
THEN (RWO "rmul-is-positive" (-1) THENM D -1)
THEN Auto)
Home
Index