isTrichotomous — Mathlib

English

If a relation on α is trichotomous and f: β → α is injective, then the inverse image relation on β is trichotomous.

Русский

Если на α тричотомично и функция f: β → α инъективна, то на β образ инверсного отношения тричотомичен.

LaTeX

$$$[IsTrichotomous \\alpha \\ r] [f: \\beta \\to \\alpha] (\\text{Injective } f) \\Rightarrow IsTrichotomous \\beta (InvImage\\ r\\ f)$$$

Lean4

theorem isTrichotomous [IsTrichotomous α r] {f : β → α} (h : Function.Injective f) : IsTrichotomous β (InvImage r f)
    where trichotomous a b := trichotomous (f a) (f b) |>.imp3 id (h ·) id

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