English
An AddTorsor over a connected group is connected.
Русский
Адд-торсор над связной группой является связным пространством.
LaTeX
$$ConnectedSpace P$$
Lean4
/-- An `AddTorsor` for a connected space is a connected space. This is not an instance because
it loops for a group as a torsor over itself. -/
protected theorem connectedSpace : ConnectedSpace P :=
{ isPreconnected_univ :=
by
convert
isPreconnected_univ.image (Equiv.vaddConst (Classical.arbitrary P) : G → P)
(continuous_id.vadd continuous_const).continuousOn
rw [Set.image_univ, Equiv.range_eq_univ]
toNonempty := inferInstance }