isBlock_top — Mathlib

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

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