Documentation

Mathlib.Topology.Clopen

Clopen sets #

A clopen set is a set that is both closed and open.

theorem IsClopen.isOpen {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsClopen s) :
theorem IsClopen.isClosed {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsClopen s) :
@[simp]
theorem IsClopen.frontier_eq {X : Type u} [TopologicalSpace X] {s : Set X} :

Alias of the forward direction of isClopen_iff_frontier_eq_empty.

theorem IsClopen.union {X : Type u} [TopologicalSpace X] {s : Set X} {t : Set X} (hs : IsClopen s) (ht : IsClopen t) :
theorem IsClopen.inter {X : Type u} [TopologicalSpace X] {s : Set X} {t : Set X} (hs : IsClopen s) (ht : IsClopen t) :
theorem isClopen_univ {X : Type u} [TopologicalSpace X] :
IsClopen Set.univ
theorem IsClopen.compl {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsClopen s) :
@[simp]
theorem IsClopen.diff {X : Type u} [TopologicalSpace X] {s : Set X} {t : Set X} (hs : IsClopen s) (ht : IsClopen t) :
IsClopen (s \ t)
theorem IsClopen.prod {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {t : Set Y} (hs : IsClopen s) (ht : IsClopen t) :
theorem isClopen_iUnion_of_finite {X : Type u} {Y : Type v} [TopologicalSpace X] [Finite Y] {s : YSet X} (h : ∀ (i : Y), IsClopen (s i)) :
IsClopen (⋃ (i : Y), s i)
theorem Set.Finite.isClopen_biUnion {X : Type u} {Y : Type v} [TopologicalSpace X] {s : Set Y} {f : YSet X} (hs : Set.Finite s) (h : is, IsClopen (f i)) :
IsClopen (⋃ i ∈ s, f i)
theorem isClopen_biUnion_finset {X : Type u} {Y : Type v} [TopologicalSpace X] {s : Finset Y} {f : YSet X} (h : is, IsClopen (f i)) :
IsClopen (⋃ i ∈ s, f i)
theorem isClopen_iInter_of_finite {X : Type u} {Y : Type v} [TopologicalSpace X] [Finite Y] {s : YSet X} (h : ∀ (i : Y), IsClopen (s i)) :
IsClopen (⋂ (i : Y), s i)
theorem Set.Finite.isClopen_biInter {X : Type u} {Y : Type v} [TopologicalSpace X] {s : Set Y} (hs : Set.Finite s) {f : YSet X} (h : is, IsClopen (f i)) :
IsClopen (⋂ i ∈ s, f i)
theorem isClopen_biInter_finset {X : Type u} {Y : Type v} [TopologicalSpace X] {s : Finset Y} {f : YSet X} (h : is, IsClopen (f i)) :
IsClopen (⋂ i ∈ s, f i)
theorem IsClopen.preimage {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Set Y} (h : IsClopen s) {f : XY} (hf : Continuous f) :
theorem ContinuousOn.preimage_isClopen_of_isClopen {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} {s : Set X} {t : Set Y} (hf : ContinuousOn f s) (hs : IsClopen s) (ht : IsClopen t) :
theorem isClopen_inter_of_disjoint_cover_clopen {X : Type u} [TopologicalSpace X] {s : Set X} {a : Set X} {b : Set X} (h : IsClopen s) (cover : s a b) (ha : IsOpen a) (hb : IsOpen b) (hab : Disjoint a b) :

The intersection of a disjoint covering by two open sets of a clopen set will be clopen.

@[simp]
theorem isClopen_range_sigmaMk {ι : Type u_1} {X : ιType u_2} [(i : ι) → TopologicalSpace (X i)] {i : ι} :
theorem QuotientMap.isClopen_preimage {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (hf : QuotientMap f) {s : Set Y} :