reflTransGen_closed — Mathlib

English

If every r-step yields a ReflTransGen p-step, then any ReflTransGen r-path yields a p-path.

Русский

Если каждый шаг r даёт путь p, то любая цепь ReflTransGen r даёт путь p.

LaTeX

$$$$\\forall {p : \\alpha \\to \\alpha \\to \\mathrm{Prop}} : (\\forall a b, r a b \\to \\operatorname{ReflTransGen} p a b) \\to \\operatorname{ReflTransGen} r a b \\to \\operatorname{ReflTransGen} p a b$$$$

Lean4

theorem reflTransGen_closed {p : α → α → Prop} :
    (∀ a b, r a b → ReflTransGen p a b) → ReflTransGen r a b → ReflTransGen p a b :=
  ReflTransGen.lift' id

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