English
Let p and q be polynomials over K with q ≠ 0, and let f be a function of two polynomial arguments into some set P, together with a compatibility condition f(p, 0) = f(0, 1) for all p, and f(a p, a q) = f(p, q) whenever q ≠ 0 and a ≠ 0. Then the value of the lifted function at the fraction p/q equals f(p, q).
Русский
Пусть p и q будут многочленами над полем K с q ≠ 0, и пусть f: (K[X] × K[X]) → P удовлетворяет совместимости: f(p, 0) = f(0, 1) для всех p и f(a p, a q) = f(p, q) при q ≠ 0 и a ≠ 0. Тогда значение поднятой функции в дроби p/q равно f(p, q).
LaTeX
$$$(\\mathrm{RatFunc.mk}\\,p\\,q).liftOn'\\,f\\,H = f\\,p\\,q$$$
Lean4
theorem liftOn'_mk {P : Sort v} (p q : K[X]) (f : K[X] → K[X] → P) (f0 : ∀ p, f p 0 = f 0 1)
(H : ∀ {p q a} (_hq : q ≠ 0) (_ha : a ≠ 0), f (a * p) (a * q) = f p q) : (RatFunc.mk p q).liftOn' f @H = f p q :=
by
rw [RatFunc.liftOn', RatFunc.liftOn_mk _ _ _ f0]
apply liftOn_condition_of_liftOn'_condition H
