closed' — Mathlib

English

If predicate P on α satisfies that r-steps preserve P in the backward direction, and h maps TransGen r a b, then P b implies P a.

Русский

Если предикат P на α удовлетворяет условию, что r-шаги сохраняют P в обратном направлении, и h применяется к TransGen r a b, то P b ⇒ P a.

LaTeX

$$$$\\forall {P:\\\\alpha \\\\to \\\\mathrm{Prop}}, (dc:\\\\forall {a b}, r a b \\\\to P b \\\\to P a)) \\\\to {a b:\\\\alpha} (h : \\\\operatorname{TransGen} r a b) \\\\to P b \\\\to P a$$$$

Lean4

theorem closed' {P : α → Prop} (dc : ∀ {a b}, r a b → P b → P a) {a b : α} (h : TransGen r a b) : P b → P a :=
  h.head_induction_on dc fun hr _ hi ↦ dc hr ∘ hi

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