liftOn_condition_of_liftOn'_condition

English

A conditional lifting principle: if H preserves the equivalence under scaling, then f(p,q) = f(p',q') when q' p = q p'.

Русский

Условный принцип подъема: если H сохраняет эквивалентность при масштабировании, то f(p,q) = f(p',q') при условии q' p = q p'.

LaTeX

$$$\\forall p,q,p',q'\\, (hq:hq \\text{ terms})\\; (h:\\; q' p = q p') \\Rightarrow f p q = f p' q'$$$

Lean4

theorem liftOn_condition_of_liftOn'_condition {P : Sort v} {f : K[X] → K[X] → P}
    (H : ∀ {p q a} (_ : q ≠ 0) (_ha : a ≠ 0), f (a * p) (a * q) = f p q) ⦃p q p' q' : K[X]⦄ (hq : q ≠ 0) (hq' : q' ≠ 0)
    (h : q' * p = q * p') : f p q = f p' q' :=
  calc
    f p q = f (q' * p) (q' * q) := (H hq hq').symm
    _ = f (q * p') (q * q') := by rw [h, mul_comm q']
    _ = f p' q' := H hq' hq

Похожие утверждения