isConnected

Mathlib.Topology.Connected.Basic

URI: https://scilib.ai/kg/mathlib#IsIrreducible.isConnected

English

If S is irreducible, then S is connected.

Русский

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

LaTeX

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

Lean4

theorem isConnected {s : Set α} (H : IsIrreducible s) : IsConnected s :=
  ⟨H.nonempty, H.isPreirreducible.isPreconnected⟩

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

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

Разделы

Аффилиация

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