transGen_minimal — Mathlib

English

If r' is transitive and contains r, then every r-derivation is also an r'-derivation, provided r ⊆ r'.

Русский

Если r' является транзитивным и содержит r, то любая цепочка по r является цепочкой по r', если r ⊆ r'.

LaTeX

$$$$\\forall {α} {r r' : α \\to α \\to \\mathrm{Prop}}, \\mathrm{Transitive}\ r' \\to (\\forall x y, r x y \\to r' x y) \\\\to \\forall {x y}, \\operatorname{TransGen} r x y \\to r' x y$$$$

Lean4

theorem transGen_minimal {r' : α → α → Prop} (hr' : Transitive r') (h : ∀ x y, r x y → r' x y) {x y : α}
    (hxy : TransGen r x y) : r' x y := by simpa [transGen_eq_self hr'] using TransGen.mono h hxy

Похожие утверждения