English
Let U be preconnected. If U ⊆ a ∪ b and both U ∩ derivedSet(a) and U ∩ derivedSet(b) are nonempty, then U ∩ (derivedSet(a) ∩ derivedSet(b)) is nonempty (under T1 assumptions).
Русский
Пусть U предсоединено. Если U ⊆ a ∪ b и оба пересечения U с производными a и b непусты, то пересечение U с производными a и b также непусто (при предположении T1).
LaTeX
$$$$\text{IsPreconnected}(U) \rightarrow (U \subseteq a \cup b) \rightarrow (U \cap \operatorname{derivedSet}(a)) \neq \emptyset \rightarrow (U \cap \operatorname{derivedSet}(b)) \neq \emptyset \rightarrow (U \cap (\operatorname{derivedSet}(a) \cap \operatorname{derivedSet}(b))).\neq \emptyset.$$$$
Lean4
theorem inter_derivedSet_nonempty [T1Space X] {U : Set X} (hs : IsPreconnected U) (a b : Set X) (h : U ⊆ a ∪ b)
(ha : (U ∩ derivedSet a).Nonempty) (hb : (U ∩ derivedSet b).Nonempty) :
(U ∩ (derivedSet a ∩ derivedSet b)).Nonempty :=
by
by_cases hu : U.Nontrivial
· apply isPreconnected_closed_iff.mp hs
· simp
· simp
· trans derivedSet U
· apply hs.preperfect_of_nontrivial hu
· rw [← derivedSet_union]
exact derivedSet_mono _ _ h
· exact ha
· exact hb
· obtain ⟨x, hx⟩ := ha.left.exists_eq_singleton_or_nontrivial.resolve_right hu
simp_all
