instWellFoundedGT — Mathlib

English

If α has a well-founded GT relation, then WithTop α has a well-founded GT relation.

Русский

Если у α есть хорошо основанное отношение '>' и соответствующее, то WithTop α имеет хорошо основанное отношение '>'.

LaTeX

$$$\\operatorname{WellFoundedGT}(\\mathrm{WithTop}\\,\\alpha)$ provided $\\operatorname{WellFoundedGT}(\\alpha)$.$$

Lean4

instance instWellFoundedGT [LT α] [WellFoundedGT α] : WellFoundedGT (WithTop α) :=
  inferInstanceAs <| WellFoundedGT (WithBot αᵒᵈ)ᵒᵈ

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