not_acc — Mathlib

English

If α has LT and NoMinOrder, then no element is accessible by <, i.e., ¬Acc (<) a for all a.

Русский

Если в α есть отношение < и отсутствует минимум, то никакой элемент не является доступным по отношению <.

LaTeX

$$$\forall a:\, \neg Acc\big(\lt\cdot\lt\big) a$$$

Lean4

theorem not_acc [LT α] [NoMinOrder α] (a : α) : ¬Acc (· < ·) a := fun h => Acc.recOn h fun x _ => (exists_lt x).recOn

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