isPreirreducible_iff_forall_mem_subset_closure_singleton

English

Equivalent characterizations of Preirreducible sets in R1 spaces: S is preirreducible iff for every x∈S, S ⊆ closure {x}.

Русский

Эквивалентные характеристики преднепрерывных множеств в пространствах R1: S преднепрерывно тогда и только тогда, когда для каждого x∈S выполняется S ⊆ closure {x}.

LaTeX

$$$[R1Space X]\\; (S\\subset X)\\; IsPreirreducible S \\iff \\forall x\\in S, S \\subseteq \\overline{\\{x\\}}.$$$

Lean4

theorem isPreirreducible_iff_forall_mem_subset_closure_singleton [R1Space X] {S : Set X} :
    IsPreirreducible S ↔ ∀ x ∈ S, S ⊆ closure { x } :=
  by
  constructor
  · intro h x hx y hy
    by_contra e
    obtain ⟨U, V, hU, hV, hxU, hyV, h'⟩ := r1_separation fun h => e h.specializes.mem_closure
    exact ((h U V hU hV ⟨x, hx, hxU⟩ ⟨y, hy, hyV⟩).mono inter_subset_right).not_disjoint h'
  · intro h u v hu hv ⟨x, hxs, hxu⟩ ⟨y, hys, hyv⟩
    exact ⟨x, hxs, hxu, (specializes_iff_mem_closure.mpr (h x hxs hys)).mem_open hv hyv⟩

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