coboundariesToCocycles₂_apply — Mathlib

English

Reiterates that the coboundary-to-cocycle map on coboundaries2 acts by taking the underlying function.

Русский

Повторяется, что отображение coboundariesToCocycles2 действует через базовую функцию.

LaTeX

$$$\forall x \in \text{coboundaries}_2 A,\; (\text{coboundariesToCocycles}_2 A)(x) = x.1$$$

Lean4

@[simp]
theorem coboundariesToCocycles₂_apply (x : coboundaries₂ A) : coboundariesToCocycles₂ A x = x.1 :=
  rfl

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