English
An action of a group G on X is pretransitive iff, for a fixed a ∈ X, every x ∈ X can be reached from a by some g ∈ G with g · a = x.
Русский
Действие группы G на X пред-переносимо эквивалентно тому, что для фиксированного a ∈ X каждый элемент x ∈ X можно получить из a действием некоторого g ∈ G: g · a = x.
LaTeX
$$$ IsPretransitive(G,X) \\iff \\forall x: X, \\exists g: G, g \\cdot a = x $$$
Lean4
/-- An action of a group is pretransitive iff any element can be moved from a fixed given one. -/
@[to_additive /-- An additive action of an additive group is pretransitive
iff any element can be moved from a fixed given one. -/
]
theorem isPretransitive_iff_base (a : X) : IsPretransitive G X ↔ ∀ x : X, ∃ g : G, g • a = x
where
mp hG x := exists_smul_eq _ a x
mpr
hG :=
.mk fun x y ↦ by
obtain ⟨g, hx⟩ := hG x
obtain ⟨h, hy⟩ := hG y
exact ⟨h * g⁻¹, by rw [← hx, smul_smul, inv_mul_cancel_right, hy]⟩
