wellFoundedGT — Mathlib

English

If 𝕆 is a preorder and α has GradeOrder 𝕆 α and WellFoundedGT 𝕆, then α is WellFoundedGT.

Русский

Если 𝕆 — предпорядок, α имеет GradeOrder 𝕆 α и WellFoundedGT 𝕆, то α наследует WellFoundedGT.

LaTeX

$$$\\\\text{WellFoundedGT } α$ given $[GradeOrder 𝕆 α]$ and $[WellFoundedGT 𝕆]$$$

Lean4

theorem wellFoundedGT (𝕆 : Type*) [Preorder 𝕆] [GradeOrder 𝕆 α] [WellFoundedGT 𝕆] : WellFoundedGT α :=
  (grade_strictMono (𝕆 := 𝕆)).wellFoundedGT

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