English
If p respects r via f, then a ReflTransGen path from a to b translates to a ReflTransGen path from f a to f b.
Русский
Если p сохраняет отношение через отображение f, то путь ReflTransGen от a к b переходит в путь ReflTransGen от 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{ReflTransGen} r a b) : \\\\operatorname{ReflTransGen} 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 : ReflTransGen r a b) :
ReflTransGen p (f a) (f b) :=
ReflTransGen.trans_induction_on hab (fun _ ↦ refl) (ReflTransGen.single ∘ h _ _) fun _ _ ↦ trans
