acc — Mathlib

English

Well-foundedness of a well-order s is equivalent to well-foundedness of every r ≺i s: WF(s) ↔ ∀ α,r, r ≺i s → WF(r).

Русский

Хорошо основанность порядка s эквивалентна хорошей основанности каждого r ≺i s.

LaTeX

$$$\\mathrm{WellFounded}(s) \\iff \\forall \\alpha\\, \\forall r:\\alpha \\to \\alpha \\to \\mathrm{Prop},\\ (r \\prec_i s) \\to \\mathrm{WellFounded}(r)$$$

Lean4

protected theorem acc [IsTrans β s] (f : r ≺i s) (a : α) : Acc r a ↔ Acc s (f a) :=
  (f : r ≼i s).acc a

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