isPreconnected

Mathlib.Topology.Connected.Basic

URI: https://scilib.ai/kg/mathlib#IsConnected.isPreconnected

English

If S is connected, then S is preconnected.

Русский

Если множество связано, то оно предсоединено.

LaTeX

$$$$ \\operatorname{IsConnected}(S) \\Rightarrow \\operatorname{IsPreconnected}(S). $$$$

Lean4

theorem isPreconnected {s : Set α} (h : IsConnected s) : IsPreconnected s :=
  h.2

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

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

Разделы

Аффилиация

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