nonempty_orbit — Mathlib

English

The orbit of any element under a Monoid action is nonempty (it contains at least the element itself under the identity).

Русский

Объектная орбита любого элемента при действии моноида непустая (она содержит сам элемент под действием единицы).

LaTeX

$$$\operatorname{orbit}(M,a) \neq \varnothing$$$

Lean4

@[to_additive]
theorem nonempty_orbit (a : α) : Set.Nonempty (orbit M a) :=
  Set.range_nonempty _

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