# Clopen sets #

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

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

Alias of the forward direction of isClopen_iff_frontier_eq_empty.

theorem IsClopen.union {X : Type u} [] {s : Set X} {t : Set X} (hs : ) (ht : ) :
theorem IsClopen.inter {X : Type u} [] {s : Set X} {t : Set X} (hs : ) (ht : ) :
theorem isClopen_empty {X : Type u} [] :
theorem isClopen_univ {X : Type u} [] :
IsClopen Set.univ
theorem IsClopen.compl {X : Type u} [] {s : Set X} (hs : ) :
@[simp]
theorem isClopen_compl_iff {X : Type u} [] {s : Set X} :
theorem IsClopen.diff {X : Type u} [] {s : Set X} {t : Set X} (hs : ) (ht : ) :
IsClopen (s \ t)
theorem IsClopen.prod {X : Type u} {Y : Type v} [] [] {s : Set X} {t : Set Y} (hs : ) (ht : ) :
theorem isClopen_iUnion_of_finite {X : Type u} {Y : Type v} [] [] {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} [] {s : Set Y} {f : YSet X} (hs : s.Finite) (h : is, IsClopen (f i)) :
IsClopen (is, f i)
theorem isClopen_biUnion_finset {X : Type u} {Y : Type v} [] {s : } {f : YSet X} (h : is, IsClopen (f i)) :
IsClopen (is, f i)
theorem isClopen_iInter_of_finite {X : Type u} {Y : Type v} [] [] {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} [] {s : Set Y} (hs : s.Finite) {f : YSet X} (h : is, IsClopen (f i)) :
IsClopen (is, f i)
theorem isClopen_biInter_finset {X : Type u} {Y : Type v} [] {s : } {f : YSet X} (h : is, IsClopen (f i)) :
IsClopen (is, f i)
theorem IsClopen.preimage {X : Type u} {Y : Type v} [] [] {s : Set Y} (h : ) {f : XY} (hf : ) :
theorem ContinuousOn.preimage_isClopen_of_isClopen {X : Type u} {Y : Type v} [] [] {f : XY} {s : Set X} {t : Set Y} (hf : ) (hs : ) (ht : ) :
theorem isClopen_inter_of_disjoint_cover_clopen {X : Type u} [] {s : Set X} {a : Set X} {b : Set X} (h : ) (cover : s a b) (ha : ) (hb : ) (hab : Disjoint a b) :

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

@[simp]
theorem isClopen_discrete {X : Type u} [] [] (s : Set X) :
theorem isClopen_range_inl {X : Type u} {Y : Type v} [] [] :
theorem isClopen_range_inr {X : Type u} {Y : Type v} [] [] :
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} [] [] {f : XY} (hf : ) {s : Set Y} :
theorem continuous_boolIndicator_iff_isClopen {X : Type u} [] (U : Set X) :
Continuous U.boolIndicator
theorem continuousOn_boolIndicator_iff_isClopen {X : Type u} [] (s : Set X) (U : Set X) :
ContinuousOn U.boolIndicator s IsClopen (Subtype.val ⁻¹' U)