English
The same lifting principle as above, but with a strengthened hypothesis: if for all a,b we have r a b → TransGen p (f a) (f b), and hab holds, then TransGen p (f a) (f b).
Русский
То же самое поднятие, но с усиленным предположением: если для всех a,b верно r a b → TransGen p (f a) (f b), и выполняется hab, то TransGen p (f a) (f b).
LaTeX
$$$$\\forall {p:\\\\beta \\\\to \\\\beta \\\\to \\\\mathrm{Prop}} {a b:\\\\alpha} (f:\\\\alpha \\\\to \\\\beta) (h:\\\\forall a b, r a b \\\\to TransGen p (f a) (f b)) (hab : \\\\operatorname{TransGen} r a b) : \\\\operatorname{TransGen} p (f a) (f b)$$$$
Lean4
theorem lift' {p : β → β → Prop} {a b : α} (f : α → β) (h : ∀ a b, r a b → TransGen p (f a) (f b))
(hab : TransGen r a b) : TransGen p (f a) (f b) := by simpa [transGen_idem] using hab.lift f h
