English
A set s is preconnected iff for all closed sets t, t', with s ⊆ t ∪ t', if s ∩ t and s ∩ t' are nonempty, then s ∩ (t ∩ t') is nonempty.
Русский
Множество s предсвязно тогда, когда для любых замкнутых t,t' с s ⊆ t ∪ t', не пусто пересечение с обоими, иначе пересечение всех трёх пусто.
LaTeX
$$$\\mathrm{IsPreconnected}(s) \\iff \\forall t,t',\\; \\mathrm{IsClosed}(t) \\land \\mathrm{IsClosed}(t') \\land s \\subseteq t \\cup t' \\Rightarrow (s \\cap t) \\neq \\varnothing \\Rightarrow (s \\cap t') \\neq \\varnothing \\Rightarrow (s \\cap (t \\cap t')) \\neq \\varnothing$$$
Lean4
theorem isPreconnected_closed_iff {s : Set α} :
IsPreconnected s ↔
∀ t t', IsClosed t → IsClosed t' → s ⊆ t ∪ t' → (s ∩ t).Nonempty → (s ∩ t').Nonempty → (s ∩ (t ∩ t')).Nonempty :=
⟨by
rintro h t t' ht ht' htt' ⟨x, xs, xt⟩ ⟨y, ys, yt'⟩
rw [← not_disjoint_iff_nonempty_inter, ← subset_compl_iff_disjoint_right, compl_inter]
intro h'
have xt' : x ∉ t' := (h' xs).resolve_left (absurd xt)
have yt : y ∉ t := (h' ys).resolve_right (absurd yt')
have := h _ _ ht.isOpen_compl ht'.isOpen_compl h' ⟨y, ys, yt⟩ ⟨x, xs, xt'⟩
rw [← compl_union] at this
exact this.ne_empty htt'.disjoint_compl_right.inter_eq,
by
rintro h u v hu hv huv ⟨x, xs, xu⟩ ⟨y, ys, yv⟩
rw [← not_disjoint_iff_nonempty_inter, ← subset_compl_iff_disjoint_right, compl_inter]
intro h'
have xv : x ∉ v := (h' xs).elim (absurd xu) id
have yu : y ∉ u := (h' ys).elim id (absurd yv)
have := h _ _ hu.isClosed_compl hv.isClosed_compl h' ⟨y, ys, yu⟩ ⟨x, xs, xv⟩
rw [← compl_union] at this
exact this.ne_empty huv.disjoint_compl_right.inter_eq⟩
