English
For a SubMulAction C and a set B ⊆ C, the block status is preserved under the inclusion map: IsBlock G (Subtype.val '' B) is equivalent to IsBlock G B.
Русский
Для SubMulAction C и множества B ⊆ C свойство блока сохраняется под отображением включения: IsBlock G (Subtype.val '' B) эквівалентно IsBlock G B.
LaTeX
$$$IsBlock(G,\\operatorname{Subtype.val} '' B) \\;\\Leftrightarrow\\; IsBlock(G, B)$$
Lean4
@[to_additive]
theorem isBlock_subtypeVal {C : SubMulAction G X} {B : Set C} : IsBlock G (Subtype.val '' B : Set X) ↔ IsBlock G B :=
by
refine forall₂_congr fun g₁ g₂ ↦ ?_
rw [← SubMulAction.inclusion.coe_eq, ← image_smul_set, ← image_smul_set, ne_eq,
Set.image_eq_image C.inclusion_injective, disjoint_image_iff C.inclusion_injective]
