finite_mulAction_orbit — Mathlib

English

Let M be a finite monoid acting on α. Then for every a in α, the orbit of a under M is a finite set.

Русский

Пусть M — конечный моноид, действующий на β. Тогда орбита любого элемента под действием M конечна.

LaTeX

$$$ \forall a \in \alpha\, ,\ Fin(\operatorname{orbit} M a). $$$

Lean4

@[to_additive]
theorem _root_.Finite.finite_mulAction_orbit [Finite M] (a : α) : Set.Finite (orbit M a) :=
  Set.finite_range _

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