English
A set B is a block for the action of the whole group ⊤ if and only if B is a block for the given group G.
Русский
Для множества B условие, что B является блоком для действия всей группы ⊤, эквивалентно тому, что B является блоком для группы G.
LaTeX
$$$IsBlock(\top:\ Subgroup\ G)\ B\ \iff\ IsBlock\ G\ B$$
Lean4
@[to_additive]
theorem isBlock_top : IsBlock (⊤ : Subgroup G) B ↔ IsBlock G B :=
Subgroup.topEquiv.toEquiv.forall_congr fun _ ↦ Subgroup.topEquiv.toEquiv.forall_congr_left