instPreorderShrink — Mathlib

English

If α is a type with Small, then Shrink α inherits a preorder structure from α.

Русский

Если α — тип с малым размером, то Shrink α наследует из α порядок.

LaTeX

$$$[\text{Preorder } α] \Rightarrow [\text{Preorder } (Shrink.\,α)]$$$

Lean4

instance [Preorder α] : Preorder (Shrink.{u} α)
    where
  le a b := (equivShrink α).symm a ≤ (equivShrink _).symm b
  le_refl a := le_refl _
  le_trans _ _ _ h₁ h₂ := h₁.trans h₂

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