English
A technical auxiliary lemma ensuring non-emptiness of intersections under a partition by closed sets.
Русский
Вспомогательная лемма, гарантирующая непустость пересечений при разбиении на замкнутые множества.
LaTeX
$$$(x,y,s,t)\text{ with } x\le y \land IsClosed(s) \land IsClosed(t) \land Icc(a,b)\subseteq s\cup t \Rightarrow (Icc(a,b)\cap s\cap t)\neq \emptyset$$$
Lean4
theorem isPreconnected_Icc_aux (x y : α) (s t : Set α) (hxy : x ≤ y) (hs : IsClosed s) (ht : IsClosed t)
(hab : Icc a b ⊆ s ∪ t) (hx : x ∈ Icc a b ∩ s) (hy : y ∈ Icc a b ∩ t) : (Icc a b ∩ (s ∩ t)).Nonempty :=
by
have xyab : Icc x y ⊆ Icc a b := Icc_subset_Icc hx.1.1 hy.1.2
by_contra hst
suffices Icc x y ⊆ s from hst ⟨y, xyab <| right_mem_Icc.2 hxy, this <| right_mem_Icc.2 hxy, hy.2⟩
apply (IsClosed.inter hs isClosed_Icc).Icc_subset_of_forall_mem_nhdsWithin hx.2
rintro z ⟨zs, hz⟩
have zt : z ∈ tᶜ := fun zt => hst ⟨z, xyab <| Ico_subset_Icc_self hz, zs, zt⟩
have : tᶜ ∩ Ioc z y ∈ 𝓝[>] z := by
rw [← nhdsWithin_Ioc_eq_nhdsGT hz.2]
exact mem_nhdsWithin.2 ⟨tᶜ, ht.isOpen_compl, zt, Subset.rfl⟩
apply mem_of_superset this
have : Ioc z y ⊆ s ∪ t := fun w hw => hab (xyab ⟨le_trans hz.1 (le_of_lt hw.1), hw.2⟩)
exact fun w ⟨wt, wzy⟩ => (this wzy).elim id fun h => (wt h).elim
