WellFoundedOn — Mathlib

English

The notion WellFoundedOn s r means that the relation r is well-founded when restricted to the set s.

Русский

Понятие WellFoundedOn s r означает, что отношение r хорошо основано при ограничении к множеству s.

LaTeX

$$WellFoundedOn(s, r) \\equiv WellFounded(Subrel(r, (\\cdot \\in s)))$$

Lean4

/-- `s.WellFoundedOn r` indicates that the relation `r` is `WellFounded` when restricted to `s`. -/
def WellFoundedOn (s : Set α) (r : α → α → Prop) : Prop :=
  WellFounded (Subrel r (· ∈ s))

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