isInvariantBlock_iff_isFixedBlock

English

An invariant block is a block.

Русский

Инвариантный блок является блоком.

LaTeX

$$$IsInvariantBlock(G,B) \Rightarrow IsBlock(G,B).$$$

Lean4

/-- A block of a group action is invariant iff it is fixed. -/
@[to_additive /-- A block of a group action is invariant iff it is fixed. -/
    ]
theorem isInvariantBlock_iff_isFixedBlock : IsInvariantBlock G B ↔ IsFixedBlock G B :=
  ⟨fun hB g ↦ (hB g).antisymm <| subset_smul_set_iff.2 <| hB _, IsFixedBlock.isInvariantBlock⟩

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