mono — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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