mono — Mathlib

English

If p is pointwise implied by r, then any TransGen derivation from a to b yields a p-derivation from a to b.

Русский

Если для любых a,b выполняется r a b → p a b, тогда любая последовательность TransGen от a к b дает последовательность p от a к b.

LaTeX

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

Lean4

theorem mono {p : α → α → Prop} : (∀ a b, r a b → p a b) → TransGen r a b → TransGen p a b :=
  TransGen.lift id

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