wellFoundedLT — Mathlib

English

If 𝕆 is a preorder and α has GradeOrder 𝕆 α and 𝕆 is well-founded with respect to <, then α is well-founded with respect to <.

Русский

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

LaTeX

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

Lean4

theorem wellFoundedLT (𝕆 : Type*) [Preorder 𝕆] [GradeOrder 𝕆 α] [WellFoundedLT 𝕆] : WellFoundedLT α :=
  (grade_strictMono (𝕆 := 𝕆)).wellFoundedLT

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