isAsymm — Mathlib

English

If a relation R on α is asymmetric, then the inverse image relation on β via any function f: β → α is asymmetric.

Русский

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

LaTeX

$$$[IsAsymm \\alpha \\ r] (f: \\beta \\to \\alpha) \\Rightarrow IsAsymm \\beta (InvImage \\ r \\ f)$$$

Lean4

instance isAsymm [IsAsymm α r] (f : β → α) : IsAsymm β (InvImage r f) where
  asymm a b h h2 := IsAsymm.asymm (f a) (f b) h h2

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