connectedSpace — Mathlib

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 }

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