wellFoundedOn_gt — Mathlib

English

If a set s is bounded above in a preorder, then s is well-founded with respect to the strict greater-than relation.

Русский

Если множество ограничено сверху в пределе порядка, тогда над отношением > множество хорошо основано.

LaTeX

$$BddAbove s \rightarrow s.WellFoundedOn (\nabla GT)$$

Lean4

theorem wellFoundedOn_gt : BddAbove s → s.WellFoundedOn (· > ·) := fun h => h.dual.wellFoundedOn_lt

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