isAntisymm — Mathlib

English

If r is antisymmetric on α, and f is injective, then the preimage order on β is antisymmetric.

Русский

Если $r$ антисимметрично на $\alpha$ и $f$ инъективен, то предобразный порядок на β антисимметричен.

LaTeX

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

Lean4

theorem isAntisymm [IsAntisymm α r] {f : β → α} (hf : f.Injective) : IsAntisymm β (f ⁻¹'o r) :=
  ⟨fun _ _ h₁ h₂ ↦ hf <| antisymm_of r h₁ h₂⟩

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