instSubsingletonQuotient — Mathlib

English

Let X be a simply connected space. Then for any two points x and y in X, the set of path classes from x to y, up to homotopy, contains at most one element.

Русский

Пусть X — просто связное пространство. Тогда между любыми двумя точками x и y пространства X множество классов путей от x к y, по гомотопии, содержит не более одного элемента.

LaTeX

$$$\forall {X} [TopologicalSpace X] [SimplyConnectedSpace X] (x : X) (y : X),\; \operatorname{Subsingleton} (Path.Homotopic.Quotient x y)$$$

Lean4

instance (x y : X) : Subsingleton (Path.Homotopic.Quotient x y) :=
  @Unique.instSubsingleton _ (Nonempty.some (by rw [simply_connected_iff_unique_homotopic] at *; tauto))

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