IsFixedBlock — Mathlib

English

A set B is G-fixed if every g ∈ G maps B to itself, i.e., g • B = B for all g.

Русский

Множество B фиксировано по действию группы, если для всех g ∈ G выполняется g • B = B.

LaTeX

$$IsFixedBlock B := ∀ g : G, g • B = B$$

Lean4

/-- A set `B` is a `G`-fixed block if `g • B = B` for all `g : G`. -/
@[to_additive /-- A set `B` is a `G`-fixed block if `g +ᵥ B = B` for all `g : G`. -/
    ]
def IsFixedBlock (B : Set X) :=
  ∀ g : G, g • B = B

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