English
An action is pretransitive if and only if the quotient by orbitRel is a subsingleton.
Русский
Действие является пре-транситивным тогда и только тогда, когда квадратно по орбитальному отношению делится на единичное множество.
LaTeX
$$IsPretransitive G α \iff Subsingleton (orbitRel.Quotient G α)$$
Lean4
/-- An action is pretransitive if and only if the quotient by `MulAction.orbitRel` is a
subsingleton. -/
@[to_additive /-- An additive action is pretransitive if and only if the quotient by
`AddAction.orbitRel` is a subsingleton. -/
]
theorem pretransitive_iff_subsingleton_quotient : IsPretransitive G α ↔ Subsingleton (orbitRel.Quotient G α) :=
by
refine ⟨fun _ ↦ ⟨fun a b ↦ ?_⟩, fun _ ↦ ⟨fun a b ↦ ?_⟩⟩
· refine Quot.inductionOn a (fun x ↦ ?_)
exact Quot.inductionOn b (fun y ↦ Quot.sound <| exists_smul_eq G y x)
· have h : Quotient.mk (orbitRel G α) b = ⟦a⟧ := Subsingleton.elim _ _
exact Quotient.eq''.mp h
