isPathConnected_singleton

Mathlib.Topology.Connected.PathConnected

URI: https://scilib.ai/kg/mathlib#isPathConnected_singleton

English

Any singleton set is path-connected.

Русский

Любое од-element множество связно по траекториям.

LaTeX

$$$$\{x\} \text{ is path-connected for any } x.$$$$

Lean4

theorem isPathConnected_singleton (x : X) : IsPathConnected ({ x } : Set X) :=
  by
  refine ⟨x, rfl, ?_⟩
  rintro y rfl
  exact JoinedIn.refl rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru