English
If r is reflexive and transitive, and r' is contained in r, and there is a ReflTransGen path from a to b via r', then r relates a to b.
Русский
Пусть r рефлексивно и транзитивно, и r' ⊆ r. Если существует путь ReflTransGen от a к b через r', то выполняется r a b.
LaTeX
$$$\\\\operatorname{ReflTransGen} r' a b \\\\Rightarrow r a b$$$
Lean4
theorem reflTransGen_of_transitive_reflexive {r' : α → α → Prop} (hr : Reflexive r) (ht : Transitive r)
(h : ∀ a b, r' a b → r a b) (h' : ReflTransGen r' a b) : r a b := by
induction h' with
| refl => exact hr _
| tail _ hbc ih => exact ht ih (h _ _ hbc)