instPredOrderShrink — Mathlib

English

If α has WellFoundedLT, then Shrink(α) also has WellFoundedLT, transported along the order isomorphism.

Русский

Если у α есть WellFoundedLT, то Shrink(α) также имеет WellFoundedLT, переносимый через порядковый изоморфизм.

LaTeX

$$$\text{WellFoundedLT}(\alpha) \Rightarrow \text{WellFoundedLT}(\operatorname{Shrink}(\alpha))$$$

Lean4

noncomputable instance [PredOrder α] : PredOrder (Shrink.{u} α) :=
  PredOrder.ofOrderIso (orderIsoShrink.{u} α)

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