instWellFoundedGT — Mathlib

English

If α carries a strict order < and WellFoundedGT α holds, then ULift α has WellFoundedGT under the induced order coming from the opposite of α.

Русский

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

LaTeX

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

Lean4

instance [LT α] [WellFoundedGT α] : WellFoundedGT (ULift α) :=
  inferInstanceAs (WellFoundedLT (ULift αᵒᵈ))

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