isAsymm — Mathlib

English

If a relation-homomorphism f preserves asymmetry from s to r, then r is asymmetrical.

Русский

Если отображение сохраняет асимметрию с s на r, то r также асимметрично.

LaTeX

$$$\forall f,\ [\text{RelHomClass } F\ r\ s] \ [\operatorname{IsAsymm} \ beta\ s] \Rightarrow \operatorname{IsAsymm} \alpha\ r$$$

Lean4

protected theorem isAsymm [RelHomClass F r s] (f : F) : ∀ [IsAsymm β s], IsAsymm α r
  | ⟨H⟩ => ⟨fun _ _ h₁ h₂ => H _ _ (map_rel f h₁) (map_rel f h₂)⟩

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