closed — Mathlib

English

Let p be a relation on α. If p extends r in the sense that r a b implies TransGen p a b, then TransGen p a b holds whenever TransGen r a b holds.

Русский

Пусть p — отношение на α. Если для любых a,b верно r a b → TransGen p a b, тогда при TransGen r a b следует TransGen p a b.

LaTeX

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

Lean4

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

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