of_subrel — Mathlib

English

Accessibility with respect to the base relation transfers from a subrelation along a fixed b.

Русский

Достижимость по базовому отношению переносится через подпорядок относительно фиксированного b.

LaTeX

$$$ Acc( r, a.1 ) \\Rightarrow Acc( Subrel\\; r\\; p, a ) $$$

Lean4

theorem of_subrel {r : α → α → Prop} [IsTrans α r] {b : α} (a : { a // r a b }) (h : Acc (Subrel r (r · b)) a) :
    Acc r a.1 :=
  h.recOn fun a _ IH ↦ ⟨_, fun _ hb ↦ IH ⟨_, _root_.trans hb a.2⟩ hb⟩

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