wellFounded_iff_wellFounded_subrel

English

A relation r on α is well-founded iff every downward interval {a | r a b} is well-founded for all b.

Русский

Отношение r на α хорошо основано тогда и только тогда, когда каждая нисходящая интервал {a | r a b} по любому b хорошо основана.

LaTeX

$$$ \\text{WellFounded}(r) \\iff \\forall b, \\text{WellFounded}(Subrel(r, r\\cdot b)). $$$

Lean4

/-- A relation `r` is well-founded iff every downward-interval `{ a | r a b }` of it is
well-founded. -/
theorem wellFounded_iff_wellFounded_subrel {r : α → α → Prop} [IsTrans α r] :
    WellFounded r ↔ ∀ b, WellFounded (Subrel r (r · b))
    where
  mp h _ := InvImage.wf Subtype.val h
  mpr h := ⟨fun a ↦ ⟨_, fun b hr ↦ ((h a).apply _).of_subrel ⟨b, hr⟩⟩⟩

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