stabilizer_isOpen — Mathlib

English

If X is discrete, the stabilizer of any x ∈ X is an open subset of M.

Русский

Если X дискретно, стабилизатор x ∈ X под действием M открыт в M.

LaTeX

$$IsOpen (MulAction.stabilizer M x)$$

Lean4

/-- The stabilizer of a continuous group action on a discrete space is an open subgroup. -/
theorem stabilizer_isOpen [DiscreteTopology X] (x : X) : IsOpen (MulAction.stabilizer M x : Set M) :=
  IsOpen.preimage (f := fun g ↦ g • x) (by fun_prop) (isOpen_discrete { x })

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