English
Let G act on X and B ⊆ X be a block for this action. If C is a subaction of X with inclusion i: C → X, then the preimage of B under i, viewed as a subset of C, is also a block for the action of G.
Русский
Пусть G действует на X, B ⊆ X является блоком для этого действия. Пусть C — поддействие X с включением i: C → X. Тогда предобраз B под i, рассматриваемый как подмножество C, тоже является блоком для действия G.
LaTeX
$$$\\text{IsBlock}(G,B) \\Rightarrow \\text{IsBlock}(G,\\operatorname{Subtype.val}^{-1} B)$$$
Lean4
@[to_additive]
theorem subtype_val_preimage {C : SubMulAction G X} (hB : IsBlock G B) : IsBlock G (Subtype.val ⁻¹' B : Set C) :=
hB.preimage C.inclusion