ext — Mathlib

English

Two n-cochains are equal if they agree on every input; i.e. if x and y lie in the nth component of the cochain object, and x(g) = y(g) for all g: Fin n → G, then x = y.

Русский

Две n-коцепы равны, если они совпадают на каждом входе; то есть если x и y принадлежат к n-му компоненту коцепного объекта и x(g) = y(g) для всех g: Fin n → G, тогда x = y.

LaTeX

$$$$ \\forall x,y \\in (\\text{inhomogeneousCochains } A)_X(n),\\ \\big( \\forall g:\\mathrm{Fin}\, n \\to G,\\ x(g)=y(g) \\big) \\Rightarrow x=y. $$$$

Lean4

@[ext]
theorem ext {x y : (inhomogeneousCochains A).X n} (h : ∀ g, x g = y g) : x = y :=
  funext h

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