English
A subset s of a densely ordered conditionally complete linear order is totally disconnected iff between any two distinct points of s there exists a point outside s within the open interval between them.
Русский
Подмножество s плотного условно полного линейного упорядоченного множества полностью несвязно тогда и только тогда, когда между любыми двумя различными точками из s лежит точка вне s внутри открытого интервала между ними.
LaTeX
$$IsTotallyDisconnected s ↔ ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∉ s, z ∈ Ioo x y$$
Lean4
/-- This lemmas characterizes when a subset `s` of a densely ordered conditionally complete linear
order is totally disconnected with respect to the order topology: between any two distinct points
of `s` must lie a point not in `s`. -/
theorem isTotallyDisconnected_iff_lt {s : Set α} :
IsTotallyDisconnected s ↔ ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∉ s, z ∈ Ioo x y :=
by
simp only [IsTotallyDisconnected, isPreconnected_iff_ordConnected, ← not_nontrivial_iff, nontrivial_iff_exists_lt,
not_exists, not_and]
refine ⟨fun h x hx y hy hxy ↦ ?_, fun h t hts ht x hx y hy hxy ↦ ?_⟩
· simp_rw [← not_ordConnected_inter_Icc_iff hx hy]
exact fun hs ↦ h _ inter_subset_left hs _ ⟨hx, le_rfl, hxy.le⟩ _ ⟨hy, hxy.le, le_rfl⟩ hxy
· obtain ⟨z, h1z, h2z⟩ := h x (hts hx) y (hts hy) hxy
exact h1z <| hts <| ht.1 hx hy ⟨h2z.1.le, h2z.2.le⟩
