IsInvariantBlock — Mathlib

English

A set B is G-invariant if for every g ∈ G we have g • B ⊆ B.

Русский

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

LaTeX

$$IsInvariantBlock B := ∀ g : G, g • B ⊆ B$$

Lean4

/-- A set `B` is a `G`-invariant block if `g • B ⊆ B` for all `g : G`.

Note: It is not necessarily a block when the action is not by a group. -/
@[to_additive /-- A set `B` is a `G`-invariant block if `g +ᵥ B ⊆ B` for all `g : G`.

    Note: It is not necessarily a block when the action is not by a group. -/
    ]
def IsInvariantBlock (B : Set X) :=
  ∀ g : G, g • B ⊆ B

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