doc-next-gen

Mathlib.Topology.Irreducible

Module docstring

{"# Irreducibility in topological spaces

Main definitions

  • IrreducibleSpace: a typeclass applying to topological spaces, stating that the space is nonempty and does not admit a nontrivial pair of disjoint opens.
  • IsIrreducible: for a nonempty set in a topological space, the property that the set is an irreducible space in the subspace topology.

On the definition of irreducible and connected sets/spaces

In informal mathematics, irreducible spaces are assumed to be nonempty. We formalise the predicate without that assumption as IsPreirreducible. In other words, the only difference is whether the empty space counts as irreducible. There are good reasons to consider the empty space to be “too simple to be simple” See also https://ncatlab.org/nlab/show/too+simple+to+be+simple, and in particular https://ncatlab.org/nlab/show/too+simple+to+be+simple#relationshiptobiased_definitions.

"}

IsPreirreducible definition
(s : Set X) : Prop
Full source 
/-- A preirreducible set `s` is one where there is no non-trivial pair of disjoint opens on `s`. -/
def IsPreirreducible (s : Set X) : Prop :=
  ∀ u v : Set X, IsOpen u → IsOpen v → (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
Preirreducible set
Informal description
A set $s$ in a topological space $X$ is called *preirreducible* if for any two open sets $u$ and $v$ in $X$, if $s$ intersects both $u$ and $v$ nontrivially, then $s$ also intersects their intersection $u \cap v$ nontrivially. In other words, there are no two disjoint open sets that both intersect $s$.
IsIrreducible definition
(s : Set X) : Prop
Full source 
/-- An irreducible set `s` is one that is nonempty and
where there is no non-trivial pair of disjoint opens on `s`. -/
def IsIrreducible (s : Set X) : Prop :=
  s.Nonempty ∧ IsPreirreducible s
Irreducible set
Informal description
A nonempty set $s$ in a topological space $X$ is called *irreducible* if it is preirreducible, meaning that for any two open sets $u$ and $v$ in $X$, if $s$ intersects both $u$ and $v$ nontrivially, then $s$ also intersects their intersection $u \cap v$ nontrivially. In other words, there are no two disjoint open sets that both intersect $s$.
IsIrreducible.nonempty theorem
(h : IsIrreducible s) : s.Nonempty
Full source 
theorem IsIrreducible.nonempty (h : IsIrreducible s) : s.Nonempty :=
  h.1
Nonemptiness of Irreducible Sets
Informal description
If a set $s$ in a topological space $X$ is irreducible, then $s$ is nonempty.
IsIrreducible.isPreirreducible theorem
(h : IsIrreducible s) : IsPreirreducible s
Full source 
theorem IsIrreducible.isPreirreducible (h : IsIrreducible s) : IsPreirreducible s :=
  h.2
Irreducible sets are preirreducible
Informal description
If a nonempty set $s$ in a topological space $X$ is irreducible, then it is preirreducible.
isPreirreducible_empty theorem
: IsPreirreducible (∅ : Set X)
Full source 
theorem isPreirreducible_empty : IsPreirreducible (∅ : Set X) := fun _ _ _ _ _ ⟨_, h1, _⟩ =>
  h1.elim
Empty Set is Preirreducible
Informal description
The empty set $\emptyset$ in a topological space $X$ is preirreducible.
isPreirreducible_iff_closure theorem
: IsPreirreducible (closure s) ↔ IsPreirreducible s
Full source 
theorem isPreirreducible_iff_closure : IsPreirreducibleIsPreirreducible (closure s) ↔ IsPreirreducible s :=
  forall₄_congr fun u v hu hv => by
    iterate 3 rw [closure_inter_open_nonempty_iff]
    exacts [hu.inter hv, hv, hu]
Preirreducibility is Equivalent to Preirreducibility of Closure
Informal description
A subset $s$ of a topological space $X$ is preirreducible if and only if its closure $\overline{s}$ is preirreducible.
exists_preirreducible theorem
(s : Set X) (H : IsPreirreducible s) : ∃ t : Set X, IsPreirreducible t ∧ s ⊆ t ∧ ∀ u, IsPreirreducible u → t ⊆ u → u = t
Full source 
theorem exists_preirreducible (s : Set X) (H : IsPreirreducible s) :
    ∃ t : Set X, IsPreirreducible t ∧ s ⊆ t ∧ ∀ u, IsPreirreducible u → t ⊆ u → u = t :=
  let ⟨m, hsm, hm⟩ :=
    zorn_subset_nonempty { t : Set X | IsPreirreducible t }
      (fun c hc hcc _ =>
        ⟨⋃₀ c, fun u v hu hv ⟨y, hy, hyu⟩ ⟨x, hx, hxv⟩ =>
          let ⟨p, hpc, hyp⟩ := mem_sUnion.1 hy
          let ⟨q, hqc, hxq⟩ := mem_sUnion.1 hx
          Or.casesOn (hcc.total hpc hqc)
            (fun hpq : p ⊆ q =>
              let ⟨x, hxp, hxuv⟩ := hc hqc u v hu hv ⟨y, hpq hyp, hyu⟩ ⟨x, hxq, hxv⟩
              ⟨x, mem_sUnion_of_mem hxp hqc, hxuv⟩)
            fun hqp : q ⊆ p =>
            let ⟨x, hxp, hxuv⟩ := hc hpc u v hu hv ⟨y, hyp, hyu⟩ ⟨x, hqp hxq, hxv⟩
            ⟨x, mem_sUnion_of_mem hxp hpc, hxuv⟩,
          fun _ hxc => subset_sUnion_of_mem hxc⟩)
      s H
  ⟨m, hm.prop, hsm, fun _u hu hmu => (hm.eq_of_subset hu hmu).symm⟩
Existence of Maximal Preirreducible Set Containing a Given Preirreducible Set
Informal description
For any preirreducible subset $s$ of a topological space $X$, there exists a maximal preirreducible subset $t$ containing $s$, meaning that $t$ is preirreducible, $s \subseteq t$, and any other preirreducible subset $u$ containing $t$ must equal $t$.
irreducibleComponents definition
(X : Type*) [TopologicalSpace X] : Set (Set X)
Full source 
/-- The set of irreducible components of a topological space. -/
def irreducibleComponents (X : Type*) [TopologicalSpace X] : Set (Set X) :=
  {s | Maximal IsIrreducible s}
Irreducible components of a topological space
Informal description
The set of irreducible components of a topological space $X$ consists of all maximal irreducible subsets of $X$, where a subset $s$ is maximal irreducible if it is irreducible and not properly contained in any other irreducible subset.
irreducibleComponents_eq_maximals_closed theorem
(X : Type*) [TopologicalSpace X] : irreducibleComponents X = {s | Maximal (fun x ↦ IsClosed x ∧ IsIrreducible x) s}
Full source 
theorem irreducibleComponents_eq_maximals_closed (X : Type*) [TopologicalSpace X] :
    irreducibleComponents X = { s | Maximal (fun x ↦ IsClosed x ∧ IsIrreducible x) s} := by
  ext s
  constructor
  · intro H
    exact ⟨⟨isClosed_of_mem_irreducibleComponents _ H, H.1⟩, fun x h e => H.2 h.2 e⟩
  · intro H
    refine ⟨H.1.2, fun x h e => ?_⟩
    have : closure x ≤ s := H.2 ⟨isClosed_closure, h.closure⟩ (e.trans subset_closure)
    exact le_trans subset_closure this
Irreducible Components as Maximal Closed Irreducible Subsets
Informal description
For any topological space $X$, the irreducible components of $X$ are precisely the maximal subsets of $X$ that are both closed and irreducible. In other words, the set of irreducible components equals the collection of all subsets $s \subseteq X$ that are maximal with respect to being closed and irreducible.
irreducibleComponent definition
(x : X) : Set X
Full source 
/-- A maximal irreducible set that contains a given point. -/
def irreducibleComponent (x : X) : Set X :=
  Classical.choose (exists_preirreducible {x} isPreirreducible_singleton)
Irreducible component containing a point
Informal description
For a given point \( x \) in a topological space \( X \), the *irreducible component* of \( x \) is the maximal preirreducible subset of \( X \) that contains \( x \). Here, a set is *preirreducible* if it cannot be covered by two disjoint nonempty open subsets of \( X \).
irreducibleComponent_property theorem
(x : X) : IsPreirreducible (irreducibleComponent x) ∧ { x } ⊆ irreducibleComponent x ∧ ∀ u, IsPreirreducible u → irreducibleComponent x ⊆ u → u = irreducibleComponent x
Full source 
theorem irreducibleComponent_property (x : X) :
    IsPreirreducibleIsPreirreducible (irreducibleComponent x) ∧
      {x} ⊆ irreducibleComponent x ∧
        ∀ u, IsPreirreducible u → irreducibleComponent x ⊆ u → u = irreducibleComponent x :=
  Classical.choose_spec (exists_preirreducible {x} isPreirreducible_singleton)
Maximality Property of Irreducible Components in Topological Spaces
Informal description
For any point $x$ in a topological space $X$, the irreducible component of $x$ is a preirreducible set containing $\{x\}$ and is maximal with respect to this property, meaning that any other preirreducible set $u$ containing the irreducible component must be equal to it.
isIrreducible_irreducibleComponent theorem
{x : X} : IsIrreducible (irreducibleComponent x)
Full source 
theorem isIrreducible_irreducibleComponent {x : X} : IsIrreducible (irreducibleComponent x) :=
  ⟨⟨x, mem_irreducibleComponent⟩, (irreducibleComponent_property x).1⟩
Irreducibility of the Irreducible Component
Informal description
For any point $x$ in a topological space $X$, the irreducible component of $x$ is an irreducible set. That is, it is nonempty and cannot be covered by two disjoint nonempty open subsets of $X$.
irreducibleComponent_mem_irreducibleComponents theorem
(x : X) : irreducibleComponent x ∈ irreducibleComponents X
Full source 
theorem irreducibleComponent_mem_irreducibleComponents (x : X) :
    irreducibleComponentirreducibleComponent x ∈ irreducibleComponents X :=
  ⟨isIrreducible_irreducibleComponent, fun _ h₁ h₂ => (eq_irreducibleComponent h₁.2 h₂).le⟩
Irreducible Component Membership in Irreducible Components
Informal description
For any point $x$ in a topological space $X$, the irreducible component containing $x$ is a member of the set of all irreducible components of $X$.
PreirreducibleSpace structure
(X : Type*) [TopologicalSpace X]
Full source 
/-- A preirreducible space is one where there is no non-trivial pair of disjoint opens. -/
class PreirreducibleSpace (X : Type*) [TopologicalSpace X] : Prop where
  /-- In a preirreducible space, `Set.univ` is a preirreducible set. -/
  isPreirreducible_univ : IsPreirreducible (univ : Set X)
Preirreducible topological space
Informal description
A preirreducible space is a topological space \( X \) where there are no non-trivial pairs of disjoint open sets. That is, any two non-empty open sets in \( X \) must intersect.
IrreducibleSpace structure
(X : Type*) [TopologicalSpace X] : Prop extends PreirreducibleSpace X
Full source 
/-- An irreducible space is one that is nonempty
and where there is no non-trivial pair of disjoint opens. -/
class IrreducibleSpace (X : Type*) [TopologicalSpace X] : Prop extends PreirreducibleSpace X where
  toNonempty : Nonempty X
Irreducible topological space
Informal description
A topological space \( X \) is called *irreducible* if it is nonempty and cannot be written as the union of two nonempty disjoint open sets. In other words, any two nonempty open sets in \( X \) must intersect.
IrreducibleSpace.isIrreducible_univ theorem
(X : Type*) [TopologicalSpace X] [IrreducibleSpace X] : IsIrreducible (univ : Set X)
Full source 
theorem IrreducibleSpace.isIrreducible_univ (X : Type*) [TopologicalSpace X] [IrreducibleSpace X] :
    IsIrreducible (univ : Set X) :=
  ⟨univ_nonempty, PreirreducibleSpace.isPreirreducible_univ⟩
Universal Set is Irreducible in Irreducible Space
Informal description
For any topological space $X$ that is irreducible, the universal set $\text{univ} = X$ is irreducible as a subset of $X$.
irreducibleSpace_def theorem
(X : Type*) [TopologicalSpace X] : IrreducibleSpace X ↔ IsIrreducible (⊤ : Set X)
Full source 
theorem irreducibleSpace_def (X : Type*) [TopologicalSpace X] :
    IrreducibleSpaceIrreducibleSpace X ↔ IsIrreducible (⊤ : Set X) :=
  ⟨@IrreducibleSpace.isIrreducible_univ X _, fun h =>
    haveI : PreirreducibleSpace X := ⟨h.2⟩
    ⟨⟨h.1.some⟩⟩⟩
Characterization of Irreducible Spaces via Universal Set
Informal description
A topological space $X$ is irreducible if and only if the universal set $\text{univ} = X$ is irreducible as a subset of $X$.
nonempty_preirreducible_inter theorem
[PreirreducibleSpace X] : IsOpen s → IsOpen t → s.Nonempty → t.Nonempty → (s ∩ t).Nonempty
Full source 
theorem nonempty_preirreducible_inter [PreirreducibleSpace X] :
    IsOpen s → IsOpen t → s.Nonempty → t.Nonempty → (s ∩ t).Nonempty := by
  simpa only [univ_inter, univ_subset_iff] using
    @PreirreducibleSpace.isPreirreducible_univ X _ _ s t
Nonempty Intersection of Nonempty Open Sets in Preirreducible Space
Informal description
Let \( X \) be a preirreducible topological space. For any two nonempty open sets \( s \) and \( t \) in \( X \), their intersection \( s \cap t \) is nonempty.
IsOpen.dense theorem
[PreirreducibleSpace X] (ho : IsOpen s) (hne : s.Nonempty) : Dense s
Full source 
/-- In a (pre)irreducible space, a nonempty open set is dense. -/
protected theorem IsOpen.dense [PreirreducibleSpace X] (ho : IsOpen s) (hne : s.Nonempty) :
    Dense s :=
  dense_iff_inter_open.2 fun _t hto htne => nonempty_preirreducible_inter hto ho htne hne
Nonempty Open Sets are Dense in Preirreducible Spaces
Informal description
Let $X$ be a preirreducible topological space. For any nonempty open subset $s$ of $X$, $s$ is dense in $X$.
IsPreirreducible.image theorem
(H : IsPreirreducible s) (f : X → Y) (hf : ContinuousOn f s) : IsPreirreducible (f '' s)
Full source 
theorem IsPreirreducible.image (H : IsPreirreducible s) (f : X → Y) (hf : ContinuousOn f s) :
    IsPreirreducible (f '' s) := by
  rintro u v hu hv ⟨_, ⟨⟨x, hx, rfl⟩, hxu⟩⟩ ⟨_, ⟨⟨y, hy, rfl⟩, hyv⟩⟩
  rw [← mem_preimage] at hxu hyv
  rcases continuousOn_iff'.1 hf u hu with ⟨u', hu', u'_eq⟩
  rcases continuousOn_iff'.1 hf v hv with ⟨v', hv', v'_eq⟩
  have := H u' v' hu' hv'
  rw [inter_comm s u', ← u'_eq] at this
  rw [inter_comm s v', ← v'_eq] at this
  rcases this ⟨x, hxu, hx⟩ ⟨y, hyv, hy⟩ with ⟨x, hxs, hxu', hxv'⟩
  refine ⟨f x, mem_image_of_mem f hxs, ?_, ?_⟩
  all_goals
    rw [← mem_preimage]
    apply mem_of_mem_inter_left
    show x ∈ _ ∩ s
    simp [*]
Image of a Preirreducible Set under Continuous Map is Preirreducible
Informal description
Let $X$ and $Y$ be topological spaces, and let $s \subseteq X$ be a preirreducible set. If $f : X \to Y$ is a continuous function on $s$, then the image $f(s)$ is also preirreducible in $Y$.
IsIrreducible.image theorem
(H : IsIrreducible s) (f : X → Y) (hf : ContinuousOn f s) : IsIrreducible (f '' s)
Full source 
theorem IsIrreducible.image (H : IsIrreducible s) (f : X → Y) (hf : ContinuousOn f s) :
    IsIrreducible (f '' s) :=
  ⟨H.nonempty.image _, H.isPreirreducible.image f hf⟩
Continuous Image of Irreducible Set is Irreducible
Informal description
Let $X$ and $Y$ be topological spaces, and let $s \subseteq X$ be an irreducible set. If $f : X \to Y$ is a continuous function on $s$, then the image $f(s)$ is also irreducible in $Y$.
Subtype.preirreducibleSpace theorem
(h : IsPreirreducible s) : PreirreducibleSpace s
Full source 
theorem Subtype.preirreducibleSpace (h : IsPreirreducible s) : PreirreducibleSpace s where
  isPreirreducible_univ := by
    rintro _ _ ⟨u, hu, rfl⟩ ⟨v, hv, rfl⟩ ⟨⟨x, hxs⟩, -, hxu⟩ ⟨⟨y, hys⟩, -, hyv⟩
    rcases h u v hu hv ⟨x, hxs, hxu⟩ ⟨y, hys, hyv⟩ with ⟨x, hxs, ⟨hxu, hxv⟩⟩
    exact ⟨⟨x, hxs⟩, ⟨Set.mem_univ _, ⟨hxu, hxv⟩⟩⟩
Preirreducible Subspace Induced by Preirreducible Set
Informal description
If a subset $s$ of a topological space $X$ is preirreducible, then the subspace $s$ equipped with the subspace topology is a preirreducible space.
Subtype.irreducibleSpace theorem
(h : IsIrreducible s) : IrreducibleSpace s
Full source 
theorem Subtype.irreducibleSpace (h : IsIrreducible s) : IrreducibleSpace s where
  isPreirreducible_univ :=
    (Subtype.preirreducibleSpace h.isPreirreducible).isPreirreducible_univ
  toNonempty := h.nonempty.to_subtype
Irreducible Subspace Induced by Irreducible Set
Informal description
If a subset $s$ of a topological space $X$ is irreducible, then the subspace $s$ equipped with the subspace topology is an irreducible space.
instIrreducibleSpaceCofiniteTopologyOfInfinite instance
{X} [Infinite X] : IrreducibleSpace (CofiniteTopology X)
Full source 
/-- An infinite type with cofinite topology is an irreducible topological space. -/
instance (priority := 100) {X} [Infinite X] : IrreducibleSpace (CofiniteTopology X) where
  isPreirreducible_univ u v := by
    haveI : Infinite (CofiniteTopology X) := ‹_›
    simp only [CofiniteTopology.isOpen_iff, univ_inter]
    intro hu hv hu' hv'
    simpa only [compl_union, compl_compl] using ((hu hu').union (hv hv')).infinite_compl.nonempty
  toNonempty := (inferInstance : Nonempty X)
Irreducibility of Cofinite Topology on Infinite Types
Informal description
For any infinite type $X$, the cofinite topology on $X$ is an irreducible topological space. That is, the space is nonempty and cannot be written as the union of two nonempty disjoint open sets.
irreducibleComponents_eq_singleton theorem
[IrreducibleSpace X] : irreducibleComponents X = { univ }
Full source 
theorem irreducibleComponents_eq_singleton [IrreducibleSpace X] :
    irreducibleComponents X = {univ} :=
  Set.ext fun _ ↦ IsGreatest.maximal_iff (s := IsIrreducible (X := X))
    ⟨IrreducibleSpace.isIrreducible_univ X, fun _ _ ↦ Set.subset_univ _⟩
Irreducible Space Has Single Irreducible Component
Informal description
For an irreducible topological space $X$, the set of irreducible components of $X$ is the singleton set containing the universal set, i.e., $\text{irreducibleComponents}(X) = \{X\}$.
isIrreducible_iff_sInter theorem
: IsIrreducible s ↔ ∀ (U : Finset (Set X)), (∀ u ∈ U, IsOpen u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑U).Nonempty
Full source 
/-- A set `s` is irreducible if and only if
for every finite collection of open sets all of whose members intersect `s`,
`s` also intersects the intersection of the entire collection
(i.e., there is an element of `s` contained in every member of the collection). -/
theorem isIrreducible_iff_sInter :
    IsIrreducibleIsIrreducible s ↔
      ∀ (U : Finset (Set X)), (∀ u ∈ U, IsOpen u) → (∀ u ∈ U, (s ∩ u).Nonempty) →
        (s ∩ ⋂₀ ↑U).Nonempty := by
  classical
  refine ⟨fun h U hu hU => ?_, fun h => ⟨?_, ?_⟩⟩
  · induction U using Finset.induction_on with
    | empty => simpa using h.nonempty
    | insert u U _ IH =>
      rw [Finset.coe_insert, sInter_insert]
      rw [Finset.forall_mem_insert] at hu hU
      exact h.2 _ _ hu.1 (U.finite_toSet.isOpen_sInter hu.2) hU.1 (IH hu.2 hU.2)
  · simpa using h ∅
  · intro u v hu hv hu' hv'
    simpa [*] using h {u, v}
Finite Intersection Characterization of Irreducible Sets
Informal description
A nonempty set $s$ in a topological space $X$ is irreducible if and only if for every finite collection of open sets $\{U_i\}_{i \in I}$ in $X$ such that $s \cap U_i \neq \emptyset$ for all $i \in I$, the intersection $s \cap \bigcap_{i \in I} U_i$ is also nonempty.
isPreirreducible_iff_isClosed_union_isClosed theorem
: IsPreirreducible s ↔ ∀ z₁ z₂ : Set X, IsClosed z₁ → IsClosed z₂ → s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂
Full source 
/-- A set is preirreducible if and only if
for every cover by two closed sets, it is contained in one of the two covering sets. -/
theorem isPreirreducible_iff_isClosed_union_isClosed :
    IsPreirreducibleIsPreirreducible s ↔
      ∀ z₁ z₂ : Set X, IsClosed z₁ → IsClosed z₂ → s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂ := by
  refine compl_surjective.forall.trans <| forall_congr' fun z₁ => compl_surjective.forall.trans <|
    forall_congr' fun z₂ => ?_
  simp only [isOpen_compl_iff, ← compl_union, inter_compl_nonempty_iff]
  refine forall₂_congr fun _ _ => ?_
  rw [← and_imp, ← not_or, not_imp_not]
Characterization of Preirreducible Sets via Closed Covers
Informal description
A subset $s$ of a topological space $X$ is preirreducible if and only if for any two closed subsets $z_1$ and $z_2$ of $X$ such that $s \subseteq z_1 \cup z_2$, either $s \subseteq z_1$ or $s \subseteq z_2$.
isIrreducible_iff_sUnion_isClosed theorem
: IsIrreducible s ↔ ∀ t : Finset (Set X), (∀ z ∈ t, IsClosed z) → (s ⊆ ⋃₀ ↑t) → ∃ z ∈ t, s ⊆ z
Full source 
/-- A set is irreducible if and only if for every cover by a finite collection of closed sets, it is
contained in one of the members of the collection. -/
theorem isIrreducible_iff_sUnion_isClosed :
    IsIrreducibleIsIrreducible s ↔
      ∀ t : Finset (Set X), (∀ z ∈ t, IsClosed z) → (s ⊆ ⋃₀ ↑t) → ∃ z ∈ t, s ⊆ z := by
  simp only [isIrreducible_iff_sInter]
  refine ((@compl_involutive (Set X) _).toPerm _).finsetCongr.forall_congr fun {t} => ?_
  simp_rw [Equiv.finsetCongr_apply, Finset.forall_mem_map, Finset.mem_map, Finset.coe_map,
    sUnion_image, Equiv.coe_toEmbedding, Function.Involutive.coe_toPerm, isClosed_compl_iff,
    exists_exists_and_eq_and]
  refine forall_congr' fun _ => Iff.trans ?_ not_imp_not
  simp only [not_exists, not_and, ← compl_iInter₂, ← sInter_eq_biInter,
    subset_compl_iff_disjoint_right, not_disjoint_iff_nonempty_inter]
Finite Closed Cover Characterization of Irreducible Sets
Informal description
A nonempty set $s$ in a topological space $X$ is irreducible if and only if for every finite collection $\{z_i\}_{i \in I}$ of closed sets in $X$ such that $s \subseteq \bigcup_{i \in I} z_i$, there exists some $i \in I$ such that $s \subseteq z_i$.
subset_closure_inter_of_isPreirreducible_of_isOpen theorem
{S U : Set X} (hS : IsPreirreducible S) (hU : IsOpen U) (h : (S ∩ U).Nonempty) : S ⊆ closure (S ∩ U)
Full source 
/-- A nonempty open subset of a preirreducible subspace is dense in the subspace. -/
theorem subset_closure_inter_of_isPreirreducible_of_isOpen {S U : Set X} (hS : IsPreirreducible S)
    (hU : IsOpen U) (h : (S ∩ U).Nonempty) : S ⊆ closure (S ∩ U) := by
  by_contra h'
  obtain ⟨x, h₁, h₂, h₃⟩ :=
    hS _ (closure (S ∩ U))ᶜ hU isClosed_closure.isOpen_compl h (inter_compl_nonempty_iff.mpr h')
  exact h₃ (subset_closure ⟨h₁, h₂⟩)
Density of Nonempty Open Subsets in Preirreducible Sets
Informal description
Let $S$ be a preirreducible subset of a topological space $X$, and let $U$ be an open subset of $X$ such that $S \cap U$ is nonempty. Then $S$ is contained in the closure of $S \cap U$.
IsPreirreducible.subset_irreducible theorem
{S U : Set X} (ht : IsPreirreducible t) (hU : U.Nonempty) (hU' : IsOpen U) (h₁ : U ⊆ S) (h₂ : S ⊆ t) : IsIrreducible S
Full source 
/-- If `∅ ≠ U ⊆ S ⊆ t` such that `U` is open and `t` is preirreducible, then `S` is irreducible. -/
theorem IsPreirreducible.subset_irreducible {S U : Set X} (ht : IsPreirreducible t)
    (hU : U.Nonempty) (hU' : IsOpen U) (h₁ : U ⊆ S) (h₂ : S ⊆ t) : IsIrreducible S := by
  obtain ⟨z, hz⟩ := hU
  replace ht : IsIrreducible t := ⟨⟨z, h₂ (h₁ hz)⟩, ht⟩
  refine ⟨⟨z, h₁ hz⟩, ?_⟩
  rintro u v hu hv ⟨x, hx, hx'⟩ ⟨y, hy, hy'⟩
  classical
  obtain ⟨x, -, hx'⟩ : Set.Nonempty (t ∩ ⋂₀ ↑({U, u, v} : Finset (Set X))) := by
    refine isIrreducible_iff_sInter.mp ht {U, u, v} ?_ ?_
    · simp [*]
    · intro U H
      simp only [Finset.mem_insert, Finset.mem_singleton] at H
      rcases H with (rfl | rfl | rfl)
      exacts [⟨z, h₂ (h₁ hz), hz⟩, ⟨x, h₂ hx, hx'⟩, ⟨y, h₂ hy, hy'⟩]
  replace hx' : x ∈ Ux ∈ U ∧ x ∈ u ∧ x ∈ v := by simpa using hx'
  exact ⟨x, h₁ hx'.1, hx'.2⟩
Irreducibility of Sets Containing Nonempty Open Subsets in Preirreducible Spaces
Informal description
Let $X$ be a topological space, $t \subseteq X$ a preirreducible subset, and $S \subseteq X$ a subset containing a nonempty open set $U \subseteq S \subseteq t$. Then $S$ is irreducible.
IsPreirreducible.open_subset theorem
{U : Set X} (ht : IsPreirreducible t) (hU : IsOpen U) (hU' : U ⊆ t) : IsPreirreducible U
Full source 
theorem IsPreirreducible.open_subset {U : Set X} (ht : IsPreirreducible t) (hU : IsOpen U)
    (hU' : U ⊆ t) : IsPreirreducible U :=
  U.eq_empty_or_nonempty.elim (fun h => h.symm ▸ isPreirreducible_empty) fun h =>
    (ht.subset_irreducible h hU (fun _ => id) hU').2
Open Subsets of Preirreducible Sets are Preirreducible
Informal description
Let $X$ be a topological space, $t \subseteq X$ a preirreducible subset, and $U \subseteq X$ an open subset such that $U \subseteq t$. Then $U$ is preirreducible.
IsPreirreducible.preimage theorem
(ht : IsPreirreducible t) {f : Y → X} (hf : IsOpenEmbedding f) : IsPreirreducible (f ⁻¹' t)
Full source 
theorem IsPreirreducible.preimage (ht : IsPreirreducible t) {f : Y → X}
    (hf : IsOpenEmbedding f) : IsPreirreducible (f ⁻¹' t) := by
  rintro U V hU hV ⟨x, hx, hx'⟩ ⟨y, hy, hy'⟩
  obtain ⟨_, h₁, ⟨y, h₂, rfl⟩, ⟨y', h₃, h₄⟩⟩ :=
    ht _ _ (hf.isOpenMap _ hU) (hf.isOpenMap _ hV) ⟨f x, hx, Set.mem_image_of_mem f hx'⟩
      ⟨f y, hy, Set.mem_image_of_mem f hy'⟩
  cases hf.injective h₄
  exact ⟨y, h₁, h₂, h₃⟩
Preimage of Preirreducible Set under Open Embedding is Preirreducible
Informal description
Let $t$ be a preirreducible subset of a topological space $X$, and let $f \colon Y \to X$ be an open embedding. Then the preimage $f^{-1}(t)$ is also preirreducible in $Y$.