IsFractionalPolymorphismFor — Mathlib

English

A fractional operation ω is a fractional polymorphism for a VCSP template Γ if every cost function f in Γ admits ω.

Русский

Фракционная операция ω является фракционным полиморфизмом шаблона VCSP Γ, если каждая функция затрат f из Γ допускает ω.

LaTeX

$$$\\forall f \\in Γ, f.snd.AdmitsFractional \\; ω$$$

Lean4

/-- Fractional operation is a fractional polymorphism for given VCSP template. -/
def IsFractionalPolymorphismFor (ω : FractionalOperation D m) (Γ : ValuedCSP D C) : Prop :=
  ∀ f ∈ Γ, f.snd.AdmitsFractional ω

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