English
Disjoint(ordT5Nhd(s,t), ordT5Nhd(t,s)).
Русский
Раздельность ordT5Nhd(s,t) и ordT5Nhd(t,s).
LaTeX
$$Disjoint( ordT5Nhd(s,t), ordT5Nhd(t,s) )$$
Lean4
theorem disjoint_ordT5Nhd : Disjoint (ordT5Nhd s t) (ordT5Nhd t s) :=
by
rw [disjoint_iff_inf_le]
rintro x ⟨hx₁, hx₂⟩
rcases mem_iUnion₂.1 hx₁ with ⟨a, has, ha⟩
clear hx₁
rcases mem_iUnion₂.1 hx₂ with ⟨b, hbt, hb⟩
clear hx₂
rw [mem_ordConnectedComponent, subset_inter_iff] at ha hb
wlog hab : a ≤ b with H
· exact H b hbt hb a has ha (le_of_not_ge hab)
obtain ⟨ha, ha'⟩ := ha
obtain ⟨hb, hb'⟩ := hb
have hsub : [[a, b]] ⊆ (ordSeparatingSet s t).ordConnectedSectionᶜ :=
by
rw [ordSeparatingSet_comm, uIcc_comm] at hb'
calc
[[a, b]] ⊆ [[a, x]] ∪ [[x, b]] := uIcc_subset_uIcc_union_uIcc
_ ⊆ (ordSeparatingSet s t).ordConnectedSectionᶜ := union_subset ha' hb'
clear ha' hb'
rcases le_total x a with hxa | hax
· exact hb (Icc_subset_uIcc' ⟨hxa, hab⟩) has
rcases le_total b x with hbx | hxb
· exact ha (Icc_subset_uIcc ⟨hab, hbx⟩) hbt
have h' : x ∈ ordSeparatingSet s t := ⟨mem_iUnion₂.2 ⟨a, has, ha⟩, mem_iUnion₂.2 ⟨b, hbt, hb⟩⟩
lift x to ordSeparatingSet s t using h'
suffices ordConnectedComponent (ordSeparatingSet s t) x ⊆ [[a, b]] from
hsub (this <| ordConnectedProj_mem_ordConnectedComponent _ x) (mem_range_self _)
rintro y hy
rw [uIcc_of_le hab, mem_Icc, ← not_lt, ← not_lt]
have sol1 := fun (hya : y < a) =>
(disjoint_left (t := ordSeparatingSet s t)).1 disjoint_left_ordSeparatingSet has
(hy <| Icc_subset_uIcc' ⟨hya.le, hax⟩)
have sol2 := fun (hby : b < y) =>
(disjoint_left (t := ordSeparatingSet s t)).1 disjoint_right_ordSeparatingSet hbt
(hy <| Icc_subset_uIcc ⟨hxb, hby.le⟩)
exact ⟨sol1, sol2⟩
