English
Let α be a LinearOrder with LocallyFiniteOrder. Then I is OrdConnected if and only if for all x ∈ I and y ∈ I, if the open interval Ioo(x,y) is disjoint from I, then Ioo(x,y) = ∅.
Русский
Пусть α — линейный порядок с локально конечным порядком. Тогда I является ord-connected тогда и только тогда, когда для любых x ∈ I и y ∈ I выполняется: если открытый интервал Ioo(x,y) не содержит элементов из I, то Ioo(x,y) пуст.
LaTeX
$$$\operatorname{OrdConnected}(I) \iff \forall x \in I \forall y \in I\ ( \operatorname{Disjoint}(Ioo(x,y), I) \Rightarrow Ioo(x,y) = \varnothing )$$$
Lean4
theorem ordConnected_iff_disjoint_Ioo_empty [LinearOrder α] [LocallyFiniteOrder α] :
I.OrdConnected ↔ ∀ᵉ (x ∈ I) (y ∈ I), Disjoint (Ioo x y) I → Ioo x y = ∅ :=
by
simp_rw [← Set.subset_compl_iff_disjoint_right]
refine ⟨fun h' x hx y hy hxy ↦ ?_, fun h' ↦ ordConnected_of_Ioo fun x hx y hy hxy z hz ↦ ?_⟩
· suffices ∀ z, x < z → y ≤ z by ext z; simpa using this z
intro z hz
suffices z ∉ Ioo x y by simp_all
exact fun contra ↦ hxy contra <| h'.out hx hy <| mem_Icc_of_Ioo contra
· by_contra hz'
obtain ⟨x', hx', hx''⟩ := ((finite_Icc x z).inter_of_right I).exists_le_maximal ⟨hx, le_refl _, hz.1.le⟩
have hxz : x' < z := lt_of_le_of_ne hx''.1.2.2 (ne_of_mem_of_not_mem hx''.1.1 hz')
obtain ⟨y', hy', hy''⟩ := ((finite_Icc z y).inter_of_right I).exists_le_minimal ⟨hy, hz.2.le, le_refl _⟩
have hzy : z < y' := lt_of_le_of_ne' hy''.1.2.1 (ne_of_mem_of_not_mem hy''.1.1 hz')
have h₃ : Ioc x' z ⊆ Iᶜ := fun t ht ht' ↦ hx''.not_gt (⟨ht', le_trans hx' ht.1.le, ht.2⟩) ht.1
have h₄ : Ico z y' ⊆ Iᶜ := fun t ht ht' ↦ hy''.not_lt (⟨ht', ht.1, le_trans ht.2.le hy'⟩) ht.2
have h₅ : Ioo x' y' ⊆ Iᶜ := by simp only [← Ioc_union_Ico_eq_Ioo hxz hzy, union_subset_iff, and_true, h₃, h₄]
exact eq_empty_iff_forall_notMem.1 (h' x' hx''.prop.1 y' hy''.prop.1 h₅) z ⟨hxz, hzy⟩
