isPreconnected_iff_ordConnected — Mathlib

English

Let α be a densely ordered, conditionally complete linear order with the order topology. Then for every subset s ⊆ α, IsPreconnected s if and only if OrdConnected s.

Русский

Пусть α — плотное условно полно упорядоченное линейное множество с порядковой топологией. Тогда для любого подмножества s ⊆ α выполняется: s предсоединовано тогда и только тогда, когда оно упорядочно связно.

LaTeX

$$$IsPreconnected\\ s \\iff OrdConnected\\ s$$$

Lean4

theorem isPreconnected_iff_ordConnected {s : Set α} : IsPreconnected s ↔ OrdConnected s :=
  ⟨IsPreconnected.ordConnected, Set.OrdConnected.isPreconnected⟩

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