instWellFoundedLTShrink — Mathlib

English

If α has LT, then Shrink α inherits a WellFoundedLT structure via an order isomorphism.

Русский

Если у α есть LT, то у Shrink α сохраняется структура хорошо основанного LT через отображение-изоморфизм порядка.

LaTeX

$$$[\text{WellFoundedLT } \alpha] \Rightarrow \text{WellFoundedLT}(\mathrm{Shrink}(.\,\alpha))$$$

Lean4

instance [WellFoundedLT α] : WellFoundedLT (Shrink.{u} α) where
  wf := (orderIsoShrink.{u} α).symm.toRelIsoLT.toRelEmbedding.isWellFounded.wf

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