H1π_eq_iff — Mathlib

English

For x,y in cocycles₁ A considered as a subtype, H1π A x = H1π A y iff their difference lies in coboundaries.

Русский

Для x,y в cocycles₁ A, рассмотренных как подтип, H1π A x = H1π A y тогда и только тогда, когда разность лежит в coboundaries₁ A.

LaTeX

$$theorem H1π_eq_zero_iff (x y : cocycles₁ A) : H1π A x = H1π A y ↔ ⇑x - ⇑y ∈ coboundaries₁ A$$

Lean4

theorem H1π_eq_iff (x y : cocycles₁ A) : H1π A x = H1π A y ↔ ⇑x - ⇑y ∈ coboundaries₁ A :=
  by
  rw [← sub_eq_zero, ← map_sub, H1π_eq_zero_iff]
  rfl

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