single_one_fst_sub_single_one_fst_mem_boundaries₂

English

For any group elements g,h and a in A, the combination single(1,g,h) maps into boundaries₂(A).

Русский

Для любых элементов группы g,h и a в A, элемент, задаваемый через single(1,g,h), лежит в границах₂(A).

LaTeX

$$$\text{single}(1,g,h) \; a \in boundaries_2(A)$$$

Lean4

theorem single_one_fst_sub_single_one_fst_mem_boundaries₂ (g h : G) (a : A) :
    single (1, g * h) a - single (1, g) a ∈ boundaries₂ A :=
  by
  use single (1, g, h) a
  simp [d₃₂]

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