mem_cycles₂_of_mem_boundaries₂

English

If an element lies in the boundaries at level 2, then it lies in the cycles at level 2.

Русский

Если элемент принадлежит границам на уровне 2, то он принадлежит циклам на уровне 2.

LaTeX

$$$B_2(A) \\subset Z_2(A)$$$

Lean4

theorem mem_cycles₂_of_mem_boundaries₂ (x : G × G →₀ A) (h : x ∈ boundaries₂ A) : x ∈ cycles₂ A :=
  by
  rcases h with ⟨x, rfl⟩
  exact d₃₂_apply_mem_cycles₂ x

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