orbit_eq_univ — Mathlib

English

If the action is pretransitive, then for every a ∈ α, the orbit of a under M is the entire set α.

Русский

Если действие является претранситивным, то орбита любого элемента равна всему множеству α.

LaTeX

$$$ IsPretransitive\ G\ α \Rightarrow \forall a \in \alpha,\ orbit\ M a = \operatorname{Set.univ}. $$$

Lean4

@[to_additive]
theorem orbit_eq_univ [IsPretransitive M α] (a : α) : orbit M a = Set.univ :=
  (surjective_smul M a).range_eq

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