isPretransitive_iff_orbit_eq_univ

English

A group action is pretransitive iff the orbit of a fixed element a is the entire set X.

Русский

Действие группы.pretransitive тогда и только тогда, когда орбита фиксированного элемента a равна всей X.

LaTeX

$$$ IsPretransitive(G,X) \\iff orbit(G,a) = X $$$

Lean4

/-- An action of a group is pretransitive iff the orbit of every given element is full -/
@[to_additive /-- An action of a group is pretransitive iff the orbit of every given element is full -/
    ]
theorem isPretransitive_iff_orbit_eq_univ (a : X) : IsPretransitive G X ↔ orbit G a = .univ :=
  by
  rw [isPretransitive_iff_base a, Set.ext_iff]
  apply forall_congr'
  intro x
  simp_rw [Set.mem_univ, iff_true, mem_orbit_iff]

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