instWellFoundedLT — Mathlib

English

If α has a well-founded LT relation and there is LT on α, then WithTop α inherits a well-founded LT relation.

Русский

Если у α имеется хорошо основанное отношение '<' и есть отношение LT на α, то WithTop α наследует хорошо основанное отношение '<'.

LaTeX

$$$\\operatorname{WellFoundedLT}(\\mathrm{WithTop}\\,\\alpha) \\leftarrow \\operatorname{WellFoundedLT}(\\alpha)$$$

Lean4

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

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