IsBoundary₂ — Mathlib

English

Characterization of 0-boundaries: x is a 0-boundary iff there exists a finitely supported function whose sum of differences equals x.

Русский

Характеризация нулевых границ: x является 0-гранницей тогда и только тогда, существует конечночленное отображение, чья сумма разностей равна x.

LaTeX

$$$IsBoundary_0(G,A) \iff \exists x : G \to_0 A, x.sum (\lambda g z, g \cdot z - z) = a$$$

Lean4

/-- A finsupp `x : G × G →₀ A` satisfies the 2-boundary condition if there's a finsupp
`∑ aᵢ·(gᵢ, hᵢ, jᵢ) : G × G × G →₀ A` such that
`∑ (gᵢ⁻¹ • aᵢ)·(hᵢ, jᵢ) - aᵢ·(gᵢhᵢ, jᵢ) + aᵢ·(gᵢ, hᵢjᵢ) - aᵢ·(gᵢ, hᵢ) = x.` -/
def IsBoundary₂ (x : G × G →₀ A) : Prop :=
  ∃ y : G × G × G →₀ A,
    y.sum
        (fun g a =>
          single (g.2.1, g.2.2) (g.1⁻¹ • a) - single (g.1 * g.2.1, g.2.2) a + single (g.1, g.2.1 * g.2.2) a -
            single (g.1, g.2.1) a) =
      x

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