English
A translate of a block is again a block. If B is a block for G, then g +ᵥ B is also a block for all g ∈ G.
Русский
Трансляция блока по элементу группы снова образует блок: если B — блок, то g +ᵥ B — блок для любого g ∈ G.
LaTeX
$$$IsBlock\\ G\\ B \\Rightarrow IsBlock\\ G\\ (g +\\!ᵥ B)$$$
Lean4
/-- A translate of a block is a block -/
theorem _root_.AddAction.IsBlock.translate {G : Type*} [AddGroup G] {X : Type*} [AddAction G X] (B : Set X) (g : G)
(hB : AddAction.IsBlock G B) : AddAction.IsBlock G (g +ᵥ B) :=
by
rw [← AddAction.isBlock_top] at hB ⊢
rw [← AddSubgroup.map_comap_eq_self_of_surjective (G := G) ?_ ⊤]
· apply AddAction.IsBlock.of_addSubgroup_of_conjugate
rwa [AddSubgroup.comap_top]
· exact (AddAut.conj g).surjective
