not_acc — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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