isBoundary₀_iff — Mathlib

English

An element a in A is a boundary of level 0 iff there exists x: G →₀ A with the sum over G of g·x(g) − x(g) equal to a.

Русский

Элемент a ∈ A является границей нулевого уровня тогда и только тогда, существует x: G →₀ A такое, что сумма по G от g↦(g·x(g) − x(g)) равна a.

LaTeX

$$$\\text{IsBoundary}_0\\ G\\ a \\iff \\exists x : G \\to₀ A, \\; x.sum (\\lambda g z, g \\cdot z - z) = a$$$

Lean4

theorem isBoundary₀_iff (a : A) : IsBoundary₀ G a ↔ ∃ x : G →₀ A, x.sum (fun g z => g • z - z) = a :=
  by
  constructor
  · rintro ⟨x, hx⟩
    use x.sum (fun g a => single g (-(g⁻¹ • a)))
    simp_all [sum_neg_index, sum_sum_index, neg_add_eq_sub]
  · rintro ⟨x, hx⟩
    use x.sum (fun g a => single g (-(g • a)))
    simp_all [sum_neg_index, sum_sum_index, neg_add_eq_sub]

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