instIsStrictWeakOrder — Mathlib

English

If r is a strict weak order on α, then the preimage order on β is a strict weak order.

Русский

Если $r$ является строгим слабым порядком на $\alpha$, то $f^{-1'o r}$ — строгий слабый порядок на β.

LaTeX

$$IsStrictWeakOrder(β, (f⁻¹'o r))$$

Lean4

instance instIsStrictWeakOrder [IsStrictWeakOrder α r] {f : β → α} : IsStrictWeakOrder β (f ⁻¹'o r) where
  incomp_trans _ _ _ := IsStrictWeakOrder.incomp_trans (lt := r) _ _ _

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