single_one_snd_sub_single_one_fst_mem_boundaries₂

English

Another difference of boundary-related simple elements lies in boundaries₂.

Русский

Еще одна разница простых элементов, связанных с границами, лежит в границах₂.

LaTeX

$$$\text{single}(g,1)(A.\rho g^{-1} a) - \text{single}(1,h) a \in B_2(A)$$$

Lean4

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

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