cocycles₂_ext — Mathlib

English

Two elements f1,f2 of cocycles₂ A are equal if they agree on all pairs (g,h) ∈ G × G.

Русский

Два элемента f1,f2 из cocycles₂ A равны, если они согласованы для всех пар (g,h) ∈ G × G.

LaTeX

$$$$ \forall f_1,f_2 : cocycles_2(A), \\big( \\forall g,h \\in G, f_1(g,h) = f_2(g,h) \\big) \\Rightarrow f_1 = f_2. $$$$

Lean4

@[ext]
theorem cocycles₂_ext {f₁ f₂ : cocycles₂ A} (h : ∀ g h : G, f₁ (g, h) = f₂ (g, h)) : f₁ = f₂ :=
  DFunLike.ext f₁ f₂ (Prod.forall.mpr h)

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