apply — Mathlib

English

All values are accessible under the well-founded < relation: every element can be reached by a finite descending chain.

Русский

Все значения доступны относительно хорошо основанного отношения <: каждое значение может быть достигнуто конечной нисходящей цепью.

LaTeX

$$$\\forall a:\\\\alpha,\\\\ Acc(<) a$$$

Lean4

/-- All values are accessible under the well-founded `<`. -/
theorem apply : ∀ a : α, Acc (· < ·) a :=
  IsWellFounded.apply _

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