instWellFoundedLT — Mathlib

English

Let α carry a well-founded strict order <. Then ULift α, endowed with the induced order via down, is well-founded.

Русский

Пусть у α задан строгий хорошо основанный порядок <. Тогда ULift α, на котором порядок, полученный через down, тоже хорошо основан.

LaTeX

$$$(LT\\,\\alpha) \\land (WellFoundedLT\\,\\alpha) \\Rightarrow WellFoundedLT(\\mathrm{ULift}\\,\\alpha)$$$

Lean4

instance [LT α] [h : WellFoundedLT α] : WellFoundedLT (ULift α) where wf := InvImage.wf down h.wf

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