Mathlib.Topology.Clopen

IsClopen.isOpen theorem

(hs : IsClopen s) : IsOpen s

Full source

protected theorem IsClopen.isOpen (hs : IsClopen s) : IsOpen s := hs.2

Clopen sets are open

Informal description

If a set $s$ is clopen (both closed and open), then it is open.

IsClopen.isClosed theorem

(hs : IsClopen s) : IsClosed s

Full source

protected theorem IsClopen.isClosed (hs : IsClopen s) : IsClosed s := hs.1

Clopen sets are closed

Informal description

If a set $s$ is clopen (both closed and open), then $s$ is closed.

isClopen_iff_frontier_eq_empty theorem

: IsClopen s ↔ frontier s = ∅

Full source

theorem isClopen_iff_frontier_eq_empty : IsClopenIsClopen s ↔ frontier s = ∅ := by
  rw [IsClopen, ← closure_eq_iff_isClosed, ← interior_eq_iff_isOpen, frontier, diff_eq_empty]
  refine ⟨fun h => (h.1.trans h.2.symm).subset, fun h => ?_⟩
  exact ⟨(h.trans interior_subset).antisymm subset_closure,
    interior_subset.antisymm (subset_closure.trans h)⟩

Characterization of Clopen Sets via Empty Frontier: $\text{IsClopen}(s) \leftrightarrow \text{frontier}(s) = \emptyset$

Informal description

A subset $s$ of a topological space is clopen (both closed and open) if and only if its frontier (boundary) is empty, i.e., $\text{frontier}(s) = \emptyset$.

IsClopen.union theorem

(hs : IsClopen s) (ht : IsClopen t) : IsClopen (s ∪ t)

Full source

theorem IsClopen.union (hs : IsClopen s) (ht : IsClopen t) : IsClopen (s ∪ t) :=
  ⟨hs.1.union ht.1, hs.2.union ht.2⟩

Union of Clopen Sets is Clopen

Informal description

For any two subsets $s$ and $t$ of a topological space $X$, if both $s$ and $t$ are clopen (both closed and open), then their union $s \cup t$ is also clopen.

IsClopen.inter theorem

(hs : IsClopen s) (ht : IsClopen t) : IsClopen (s ∩ t)

Full source

theorem IsClopen.inter (hs : IsClopen s) (ht : IsClopen t) : IsClopen (s ∩ t) :=
  ⟨hs.1.inter ht.1, hs.2.inter ht.2⟩

Intersection of Clopen Sets is Clopen

Informal description

For any two subsets $s$ and $t$ of a topological space $X$, if both $s$ and $t$ are clopen (both closed and open), then their intersection $s \cap t$ is also clopen.

isClopen_empty theorem

: IsClopen (∅ : Set X)

Full source

theorem isClopen_empty : IsClopen (∅ : Set X) := ⟨isClosed_empty, isOpen_empty⟩

Empty Set is Clopen

Informal description

The empty set $\emptyset$ is both closed and open in any topological space $X$.

isClopen_univ theorem

: IsClopen (univ : Set X)

Full source

theorem isClopen_univ : IsClopen (univ : Set X) := ⟨isClosed_univ, isOpen_univ⟩

Universal Set is Clopen

Informal description

The universal set $X$ in a topological space is both closed and open (clopen).

IsClopen.compl theorem

(hs : IsClopen s) : IsClopen sᶜ

Full source

theorem IsClopen.compl (hs : IsClopen s) : IsClopen sᶜ :=
  ⟨hs.2.isClosed_compl, hs.1.isOpen_compl⟩

Complement of a Clopen Set is Clopen

Informal description

If a set $s$ in a topological space is both closed and open (clopen), then its complement $s^c$ is also clopen.

isClopen_compl_iff theorem

: IsClopen sᶜ ↔ IsClopen s

Full source

@[simp]
theorem isClopen_compl_iff : IsClopenIsClopen sᶜ ↔ IsClopen s :=
  ⟨fun h => compl_compl s ▸ IsClopen.compl h, IsClopen.compl⟩

Clopen Complement Equivalence: $s^c$ is clopen $\leftrightarrow$ $s$ is clopen

Informal description

For any set $s$ in a topological space, the complement $s^c$ is clopen if and only if $s$ itself is clopen.

IsClopen.diff theorem

(hs : IsClopen s) (ht : IsClopen t) : IsClopen (s \ t)

Full source

theorem IsClopen.diff (hs : IsClopen s) (ht : IsClopen t) : IsClopen (s \ t) :=
  hs.inter ht.compl

Clopen Property Preserved Under Set Difference

Informal description

For any two subsets $s$ and $t$ of a topological space, if both $s$ and $t$ are clopen (both closed and open), then their set difference $s \setminus t$ is also clopen.

IsClopen.himp theorem

(hs : IsClopen s) (ht : IsClopen t) : IsClopen (s ⇨ t)

Full source

lemma IsClopen.himp (hs : IsClopen s) (ht : IsClopen t) : IsClopen (s ⇨ t) := by
  simpa [himp_eq] using ht.union hs.compl

Clopen Property Preserved Under Heyting Implication

Informal description

For any two subsets $s$ and $t$ of a topological space, if both $s$ and $t$ are clopen (both closed and open), then the Heyting implication $s \Rightarrow t$ (defined as $s^c \cup t$) is also clopen.

IsClopen.prod theorem

{t : Set Y} (hs : IsClopen s) (ht : IsClopen t) : IsClopen (s ×ˢ t)

Full source

theorem IsClopen.prod {t : Set Y} (hs : IsClopen s) (ht : IsClopen t) : IsClopen (s ×ˢ t) :=
  ⟨hs.1.prod ht.1, hs.2.prod ht.2⟩

Clopen Property Preserved Under Cartesian Product

Informal description

Let $s \subseteq X$ and $t \subseteq Y$ be clopen sets in topological spaces $X$ and $Y$ respectively. Then the Cartesian product $s \times t \subseteq X \times Y$ is also a clopen set.

isClopen_iUnion_of_finite theorem

{Y} [Finite Y] {s : Y → Set X} (h : ∀ i, IsClopen (s i)) : IsClopen (⋃ i, s i)

Full source

theorem isClopen_iUnion_of_finite {Y} [Finite Y] {s : Y → Set X} (h : ∀ i, IsClopen (s i)) :
    IsClopen (⋃ i, s i) :=
  ⟨isClosed_iUnion_of_finite (forall_and.1 h).1, isOpen_iUnion (forall_and.1 h).2⟩

Finite Union of Clopen Sets is Clopen

Informal description

For a finite index type $Y$ and a family of clopen sets $\{s_i\}_{i \in Y}$ in a topological space $X$, the union $\bigcup_{i \in Y} s_i$ is clopen.

Set.Finite.isClopen_biUnion theorem

{Y} {s : Set Y} {f : Y → Set X} (hs : s.Finite) (h : ∀ i ∈ s, IsClopen <| f i) : IsClopen (⋃ i ∈ s, f i)

Full source

theorem Set.Finite.isClopen_biUnion {Y} {s : Set Y} {f : Y → Set X} (hs : s.Finite)
    (h : ∀ i ∈ s, IsClopen <| f i) : IsClopen (⋃ i ∈ s, f i) :=
  ⟨hs.isClosed_biUnion fun i hi => (h i hi).1, isOpen_biUnion fun i hi => (h i hi).2⟩

Finite Union of Clopen Sets is Clopen

Informal description

Let $X$ and $Y$ be topological spaces, $s$ a finite subset of $Y$, and $\{f_i\}_{i \in s}$ a family of clopen subsets of $X$. Then the union $\bigcup_{i \in s} f_i$ is clopen in $X$.

isClopen_biUnion_finset theorem

{Y} {s : Finset Y} {f : Y → Set X} (h : ∀ i ∈ s, IsClopen <| f i) : IsClopen (⋃ i ∈ s, f i)

Full source

theorem isClopen_biUnion_finset {Y} {s : Finset Y} {f : Y → Set X}
    (h : ∀ i ∈ s, IsClopen <| f i) : IsClopen (⋃ i ∈ s, f i) :=
 s.finite_toSet.isClopen_biUnion h

Finite Union of Clopen Sets is Clopen (Finset Version)

Informal description

Let $X$ and $Y$ be topological spaces, $s$ a finite subset of $Y$ (represented as a finset), and $\{f_i\}_{i \in s}$ a family of clopen subsets of $X$. Then the union $\bigcup_{i \in s} f_i$ is clopen in $X$.

isClopen_iInter_of_finite theorem

{Y} [Finite Y] {s : Y → Set X} (h : ∀ i, IsClopen (s i)) : IsClopen (⋂ i, s i)

Full source

theorem isClopen_iInter_of_finite {Y} [Finite Y] {s : Y → Set X} (h : ∀ i, IsClopen (s i)) :
    IsClopen (⋂ i, s i) :=
  ⟨isClosed_iInter (forall_and.1 h).1, isOpen_iInter_of_finite (forall_and.1 h).2⟩

Finite Intersection of Clopen Sets is Clopen

Informal description

For a finite index type $Y$ and a family of clopen sets $\{s_i\}_{i \in Y}$ in a topological space $X$, the intersection $\bigcap_{i \in Y} s_i$ is clopen.

Set.Finite.isClopen_biInter theorem

{Y} {s : Set Y} (hs : s.Finite) {f : Y → Set X} (h : ∀ i ∈ s, IsClopen (f i)) : IsClopen (⋂ i ∈ s, f i)

Full source

theorem Set.Finite.isClopen_biInter {Y} {s : Set Y} (hs : s.Finite) {f : Y → Set X}
    (h : ∀ i ∈ s, IsClopen (f i)) : IsClopen (⋂ i ∈ s, f i) :=
  ⟨isClosed_biInter fun i hi => (h i hi).1, hs.isOpen_biInter fun i hi => (h i hi).2⟩

Finite Intersection of Clopen Sets is Clopen

Informal description

Let $X$ be a topological space and $Y$ be a type. For any finite subset $s \subseteq Y$ and any family of clopen sets $\{f_i\}_{i \in Y}$ in $X$, the intersection $\bigcap_{i \in s} f_i$ is clopen.

isClopen_biInter_finset theorem

{Y} {s : Finset Y} {f : Y → Set X} (h : ∀ i ∈ s, IsClopen (f i)) : IsClopen (⋂ i ∈ s, f i)

Full source

theorem isClopen_biInter_finset {Y} {s : Finset Y} {f : Y → Set X}
    (h : ∀ i ∈ s, IsClopen (f i)) : IsClopen (⋂ i ∈ s, f i) :=
  s.finite_toSet.isClopen_biInter h

Finite Intersection of Clopen Sets is Clopen (Finset Version)

Informal description

Let $X$ be a topological space and $Y$ be a type. For any finite subset $s \subseteq Y$ (represented as a finset) and any family of clopen sets $\{f_i\}_{i \in Y}$ in $X$, the intersection $\bigcap_{i \in s} f_i$ is clopen.

IsClopen.preimage theorem

{s : Set Y} (h : IsClopen s) {f : X → Y} (hf : Continuous f) : IsClopen (f ⁻¹' s)

Full source

theorem IsClopen.preimage {s : Set Y} (h : IsClopen s) {f : X → Y} (hf : Continuous f) :
    IsClopen (f ⁻¹' s) :=
  ⟨h.1.preimage hf, h.2.preimage hf⟩

Preimage of Clopen Set under Continuous Function is Clopen

Informal description

Let $X$ and $Y$ be topological spaces and $f : X \to Y$ be a continuous function. For any clopen set $s \subseteq Y$, the preimage $f^{-1}(s)$ is clopen in $X$.

ContinuousOn.preimage_isClopen_of_isClopen theorem

 {f : X → Y} {s : Set X} {t : Set Y} (hf : ContinuousOn f s) (hs : IsClopen s) (ht : IsClopen t) :
  IsClopen (s ∩ f ⁻¹' t)

Full source

theorem ContinuousOn.preimage_isClopen_of_isClopen {f : X → Y} {s : Set X} {t : Set Y}
    (hf : ContinuousOn f s) (hs : IsClopen s) (ht : IsClopen t) : IsClopen (s ∩ f ⁻¹' t) :=
  ⟨ContinuousOn.preimage_isClosed_of_isClosed hf hs.1 ht.1,
    ContinuousOn.isOpen_inter_preimage hf hs.2 ht.2⟩

Preimage of Clopen Set under Continuous Function on Clopen Domain is Clopen

Informal description

Let $X$ and $Y$ be topological spaces, $f : X \to Y$ a function, $s \subseteq X$ a clopen subset, and $t \subseteq Y$ a clopen subset. If $f$ is continuous on $s$, then the intersection $s \cap f^{-1}(t)$ is clopen in $X$.

isClopen_inter_of_disjoint_cover_clopen theorem

 {s a b : Set X} (h : IsClopen s) (cover : s ⊆ a ∪ b) (ha : IsOpen a) (hb : IsOpen b) (hab : Disjoint a b) :
  IsClopen (s ∩ a)

Full source

/-- The intersection of a disjoint covering by two open sets of a clopen set will be clopen. -/
theorem isClopen_inter_of_disjoint_cover_clopen {s a b : Set X} (h : IsClopen s) (cover : s ⊆ a ∪ b)
    (ha : IsOpen a) (hb : IsOpen b) (hab : Disjoint a b) : IsClopen (s ∩ a) := by
  refine ⟨?_, IsOpen.inter h.2 ha⟩
  have : IsClosed (s ∩ bᶜ) := IsClosed.inter h.1 (isClosed_compl_iff.2 hb)
  convert this using 1
  refine (inter_subset_inter_right s hab.subset_compl_right).antisymm ?_
  rintro x ⟨hx₁, hx₂⟩
  exact ⟨hx₁, by simpa [not_mem_of_mem_compl hx₂] using cover hx₁⟩

Intersection with Open Set in Disjoint Cover of Clopen Set is Clopen

Informal description

Let $X$ be a topological space and $s, a, b \subseteq X$ subsets such that: 1. $s$ is clopen (both closed and open), 2. $s \subseteq a \cup b$, 3. $a$ and $b$ are open, 4. $a$ and $b$ are disjoint ($a \cap b = \emptyset$). Then the intersection $s \cap a$ is clopen.

isClopen_of_disjoint_cover_open theorem

{a b : Set X} (cover : univ ⊆ a ∪ b) (ha : IsOpen a) (hb : IsOpen b) (hab : Disjoint a b) : IsClopen a

Full source

theorem isClopen_of_disjoint_cover_open {a b : Set X} (cover : univuniv ⊆ a ∪ b)
    (ha : IsOpen a) (hb : IsOpen b) (hab : Disjoint a b) : IsClopen a :=
  univ_inter a ▸ isClopen_inter_of_disjoint_cover_clopen isClopen_univ cover ha hb hab

Clopenness from Disjoint Open Cover of the Whole Space

Informal description

Let $X$ be a topological space and $a, b \subseteq X$ subsets such that: 1. $X = a \cup b$ (the entire space is covered by $a$ and $b$), 2. $a$ and $b$ are open, 3. $a$ and $b$ are disjoint ($a \cap b = \emptyset$). Then $a$ is clopen (both closed and open).

isClopen_discrete theorem

[DiscreteTopology X] (s : Set X) : IsClopen s

Full source

@[simp]
theorem isClopen_discrete [DiscreteTopology X] (s : Set X) : IsClopen s :=
  ⟨isClosed_discrete _, isOpen_discrete _⟩

All Subsets are Clopen in Discrete Topology

Informal description

Let $X$ be a topological space with the discrete topology. Then every subset $s \subseteq X$ is clopen (both closed and open).

isClopen_range_inl theorem

: IsClopen (range (Sum.inl : X → X ⊕ Y))

Full source

theorem isClopen_range_inl : IsClopen (range (Sum.inl : X → X ⊕ Y)) :=
  ⟨isClosed_range_inl, isOpen_range_inl⟩

Range of Left Inclusion is Clopen in Sum Space

Informal description

The range of the left inclusion function $\text{Sum.inl} : X \to X \oplus Y$ is a clopen set in the topological space $X \oplus Y$.

isClopen_range_inr theorem

: IsClopen (range (Sum.inr : Y → X ⊕ Y))

Full source

theorem isClopen_range_inr : IsClopen (range (Sum.inr : Y → X ⊕ Y)) :=
  ⟨isClosed_range_inr, isOpen_range_inr⟩

Range of Right Inclusion is Clopen in Sum Space

Informal description

The range of the right inclusion function $\text{Sum.inr} : Y \to X \oplus Y$ is a clopen set in the topological space $X \oplus Y$.

isClopen_range_sigmaMk theorem

{X : ι → Type*} [∀ i, TopologicalSpace (X i)] {i : ι} : IsClopen (Set.range (@Sigma.mk ι X i))

Full source

theorem isClopen_range_sigmaMk {X : ι → Type*} [∀ i, TopologicalSpace (X i)] {i : ι} :
    IsClopen (Set.range (@Sigma.mk ι X i)) :=
  ⟨IsClosedEmbedding.sigmaMk.isClosed_range, IsOpenEmbedding.sigmaMk.isOpen_range⟩

Canonical Sigma Inclusion Range is Clopen in Disjoint Union Topology

Informal description

For any family of topological spaces $\{X_i\}_{i \in \iota}$ indexed by a type $\iota$, and for any fixed index $i \in \iota$, the range of the canonical inclusion map $\Sigma.\text{mk}_i : X_i \to \Sigma_{j \in \iota} X_j$ is a clopen set in the disjoint union topology on $\Sigma X$.

Topology.IsQuotientMap.isClopen_preimage theorem

{f : X → Y} (hf : IsQuotientMap f) {s : Set Y} : IsClopen (f ⁻¹' s) ↔ IsClopen s

Full source

protected theorem Topology.IsQuotientMap.isClopen_preimage {f : X → Y} (hf : IsQuotientMap f)
    {s : Set Y} : IsClopenIsClopen (f ⁻¹' s) ↔ IsClopen s :=
  and_congr hf.isClosed_preimage hf.isOpen_preimage

Clopen Criterion for Preimages under Quotient Maps

Informal description

Let $f \colon X \to Y$ be a quotient map between topological spaces. For any subset $s \subseteq Y$, the preimage $f^{-1}(s)$ is clopen in $X$ if and only if $s$ is clopen in $Y$.

continuous_boolIndicator_iff_isClopen theorem

(U : Set X) : Continuous U.boolIndicator ↔ IsClopen U

Full source

theorem continuous_boolIndicator_iff_isClopen (U : Set X) :
    ContinuousContinuous U.boolIndicator ↔ IsClopen U := by
  rw [continuous_bool_rng true, preimage_boolIndicator_true]

Continuity of Boolean Indicator Function Characterizes Clopen Sets

Informal description

For any subset $U$ of a topological space $X$, the boolean indicator function of $U$ is continuous if and only if $U$ is clopen (both closed and open).

continuousOn_boolIndicator_iff_isClopen theorem

(s U : Set X) : ContinuousOn U.boolIndicator s ↔ IsClopen (((↑) : s → X) ⁻¹' U)

Full source

theorem continuousOn_boolIndicator_iff_isClopen (s U : Set X) :
    ContinuousOnContinuousOn U.boolIndicator s ↔ IsClopen (((↑) : s → X) ⁻¹' U) := by
  rw [continuousOn_iff_continuous_restrict, ← continuous_boolIndicator_iff_isClopen]
  rfl

Continuity of Boolean Indicator on Subset Characterizes Clopen Preimage

Informal description

For any subsets $s$ and $U$ of a topological space $X$, the boolean indicator function of $U$ is continuous on $s$ if and only if the preimage of $U$ under the inclusion map $s \hookrightarrow X$ is clopen in $s$ (with the subspace topology).