English
If r' is reflexive and transitive and contains r via h, then any ReflTransGen r-derivation is contained in r'.
Русский
Если r' рефлексивно и транзитивно и содержит r через h, то любая цепочка ReflTransGen r x y лежит в r'.
LaTeX
$$$$\\forall {α} {r r' : α \\to α \\to \\mathrm{Prop}}, \\text{Reflexive } r' \\to \\text{Transitive } r' \\to (\\forall x y, r x y \\to r' x y) \\to \\forall {x y}, \\operatorname{ReflTransGen} r x y \\to r' x y$$$$
Lean4
theorem reflTransGen_minimal {r' : α → α → Prop} (hr₁ : Reflexive r') (hr₂ : Transitive r') (h : ∀ x y, r x y → r' x y)
{x y : α} (hxy : ReflTransGen r x y) : r' x y := by
simpa [reflTransGen_eq_self hr₁ hr₂] using ReflTransGen.mono h hxy
