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) : IsOpen s

theorem IsClopen.isClosed {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsClopen s) : IsClosed s

theorem isClopen_iff_frontier_eq_empty {X : Type u} [TopologicalSpace X] {s : Set X} : IsClopen s ↔ frontier s = ∅

@[simp]

theorem IsClopen.frontier_eq {X : Type u} [TopologicalSpace X] {s : Set X} : IsClopen s → frontier s = ∅

Alias of the forward direction of isClopen_iff_frontier_eq_empty.

theorem IsClopen.union {X : Type u} [TopologicalSpace X] {s t : Set X} (hs : IsClopen s) (ht : IsClopen t) : IsClopen (s ∪ t)

theorem IsClopen.inter {X : Type u} [TopologicalSpace X] {s t : Set X} (hs : IsClopen s) (ht : IsClopen t) : IsClopen (s ∩ t)

theorem isClopen_empty {X : Type u} [TopologicalSpace X] : IsClopen ∅

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) : IsClopen sᶜ

@[simp]

theorem isClopen_compl_iff {X : Type u} [TopologicalSpace X] {s : Set X} : IsClopen sᶜ ↔ IsClopen s

theorem IsClopen.diff {X : Type u} [TopologicalSpace X] {s t : Set X} (hs : IsClopen s) (ht : IsClopen t) : IsClopen (s \ t)

theorem IsClopen.himp {X : Type u} [TopologicalSpace X] {s 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) : IsClopen (s ×ˢ t)

theorem isClopen_iUnion_of_finite {X : Type u} [TopologicalSpace X] {Y : Sort u_2} [Finite Y] {s : Y → Set X} (h : ∀ (i : Y), IsClopen (s i)) : IsClopen (⋃ (i : Y), s i)

theorem Set.Finite.isClopen_biUnion {X : Type u} [TopologicalSpace X] {Y : Type u_2} {s : Set Y} {f : Y → Set X} (hs : s.Finite) (h : ∀ i ∈ s, IsClopen (f i)) : IsClopen (⋃ i ∈ s, f i)

theorem isClopen_biUnion_finset {X : Type u} [TopologicalSpace X] {Y : Type u_2} {s : Finset Y} {f : Y → Set X} (h : ∀ i ∈ s, IsClopen (f i)) : IsClopen (⋃ i ∈ s, f i)

theorem isClopen_iInter_of_finite {X : Type u} [TopologicalSpace X] {Y : Sort u_2} [Finite Y] {s : Y → Set X} (h : ∀ (i : Y), IsClopen (s i)) : IsClopen (⋂ (i : Y), s i)

theorem Set.Finite.isClopen_biInter {X : Type u} [TopologicalSpace X] {Y : Type u_2} {s : Set Y} (hs : s.Finite) {f : Y → Set X} (h : ∀ i ∈ s, IsClopen (f i)) : IsClopen (⋂ i ∈ s, f i)

theorem isClopen_biInter_finset {X : Type u} [TopologicalSpace X] {Y : Type u_2} {s : Finset Y} {f : Y → Set X} (h : ∀ i ∈ s, 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 : X → Y} (hf : Continuous f) : IsClopen (f ⁻¹' s)

theorem ContinuousOn.preimage_isClopen_of_isClopen {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set X} {t : Set Y} (hf : ContinuousOn f s) (hs : IsClopen s) (ht : IsClopen t) : IsClopen (s ∩ f ⁻¹' t)

theorem isClopen_inter_of_disjoint_cover_clopen {X : Type u} [TopologicalSpace X] {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)

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

theorem isClopen_inter_of_disjoint_cover_clopen' {X : Type u} [TopologicalSpace X] {s a b : Set X} (h : IsClopen s) (cover : s ⊆ a ∪ b) (ha : IsOpen a) (hb : IsOpen b) (hab : s ∩ a ∩ b = ∅) : IsClopen (s ∩ a)

Variant of isClopen_inter_of_disjoint_cover_clopen with weaker disjointness condition.

theorem isClopen_of_disjoint_cover_open {X : Type u} [TopologicalSpace X] {a b : Set X} (cover : Set.univ ⊆ a ∪ b) (ha : IsOpen a) (hb : IsOpen b) (hab : Disjoint a b) : IsClopen a

@[simp]

theorem isClopen_discrete {X : Type u} [TopologicalSpace X] [DiscreteTopology X] (s : Set X) : IsClopen s

theorem isClopen_range_inl {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : IsClopen (Set.range Sum.inl)

theorem isClopen_range_inr {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : IsClopen (Set.range Sum.inr)

theorem isClopen_range_sigmaMk {ι : Type u_1} {X : ι → Type u_2} [(i : ι) → TopologicalSpace (X i)] {i : ι} : IsClopen (Set.range (Sigma.mk i))

theorem Topology.IsQuotientMap.isClopen_preimage {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : IsQuotientMap f) {s : Set Y} : IsClopen (f ⁻¹' s) ↔ IsClopen s

theorem continuous_boolIndicator_iff_isClopen {X : Type u} [TopologicalSpace X] (U : Set X) : Continuous U.boolIndicator ↔ IsClopen U

theorem continuousOn_boolIndicator_iff_isClopen {X : Type u} [TopologicalSpace X] (s U : Set X) : ContinuousOn U.boolIndicator s ↔ IsClopen (Subtype.val ⁻¹' U)