English
Let a,b ∈ α and f: α → β. If p is a relation on β such that p(f a, f b) whenever r a b, and hab expresses that a and b are connected by r via the transitive generator, then p relates f a to f b via its transitive generator.
Русский
Пусть a, b ∈ α и f: α → β. Пусть p — отношение на β такое, что p(f a, f b) выполняется при r a b; если a и b связаны через TransGen r, то через 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 p (f a) (f b)) (hab : \\\\operatorname{TransGen} r a b) \\\\to \\\\operatorname{TransGen} p (f a) (f b)$$$$
Lean4
theorem lift {p : β → β → Prop} {a b : α} (f : α → β) (h : ∀ a b, r a b → p (f a) (f b)) (hab : TransGen r a b) :
TransGen p (f a) (f b) := by
induction hab with
| single hac => exact TransGen.single (h a _ hac)
| tail _ hcd hac => exact TransGen.tail hac (h _ _ hcd)
