IsSymmetric — Mathlib

English

A fractional operation is a symmetric fractional polymorphism for Γ if it is both a fractional polymorphism for Γ and symmetric.

Русский

Фракционная операция образует симметричный фракционный полиморфизм для Γ, если она является полиморфизмом Γ и симметрична.

LaTeX

$$$\\text{IsSymmetricFractionalPolymorphismFor}(ω, Γ) := ω.IsFractionalPolymorphismFor(Γ) ∧ ω.IsSymmetric$$$

Lean4

/-- Fractional operation is symmetric. -/
def IsSymmetric (ω : FractionalOperation D m) : Prop :=
  ∀ x y : (Fin m → D), List.Perm (List.ofFn x) (List.ofFn y) → ∀ g ∈ ω, g x = g y

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