instWellFoundedGTOfGradeOrderOrderDualNat

English

Let α be a preorder with a grading by the dual of natural numbers. Then the greater-than relation on α is well-founded.

Русский

Пусть на α задан предорядок с градацией по обратному порядку натуральных чисел. Тогда отношение > на α хорошо основано.

LaTeX

$$$ \\operatorname{GradeOrder}(\\mathbb{N}^{\\mathrm{op}}, \\alpha) \\Rightarrow \\operatorname{WellFoundedGT}(\\alpha). $$$

Lean4

instance [GradeOrder ℕᵒᵈ α] : WellFoundedGT α :=
  GradeOrder.wellFoundedGT ℕᵒᵈ

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