isCoboundary₂_of_mem_coboundaries₂

English

Extensionality for coboundaries2: equality follows from pointwise equality of values.

Русский

Экстенсиональность coboundaries2: равенство следует из покомпонентного равенства значений.

LaTeX

$${f1 f2 : coboundaries_2 A} (∀ g,h, f1 (g,h) = f2 (g,h)) → f1 = f2$$

Lean4

theorem isCoboundary₂_of_mem_coboundaries₂ (f : G × G → A) (hf : f ∈ coboundaries₂ (Rep.ofDistribMulAction k G A)) :
    IsCoboundary₂ f := by
  rcases hf with ⟨a, rfl⟩
  exact ⟨a, fun _ _ => rfl⟩

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