subset_left_of_subset_union — Mathlib

English

If a preconnected set s intersects an open set u, and limit points of u inside s are contained in u, then s ⊆ u.

Русский

Если предсвязное множество s пересекается с открытым множеством u и все предельные точки u внутри s принадлежат u, то s ⊆ u.

LaTeX

$$$\\mathrm{IsPreconnected}(s) \\land \\mathrm{IsOpen}(u) \\land (s \\cap u) \\neq \\emptyset \\land (\\overline{u} \\cap s) \\subseteq u \\Rightarrow s \\subseteq u$$$

Lean4

theorem subset_left_of_subset_union (hu : IsOpen u) (hv : IsOpen v) (huv : Disjoint u v) (hsuv : s ⊆ u ∪ v)
    (hsu : (s ∩ u).Nonempty) (hs : IsPreconnected s) : s ⊆ u :=
  Disjoint.subset_left_of_subset_union hsuv
    (by
      by_contra hsv
      rw [not_disjoint_iff_nonempty_inter] at hsv
      obtain ⟨x, _, hx⟩ := hs u v hu hv hsuv hsu hsv
      exact Set.disjoint_iff.1 huv hx)

Похожие утверждения