Clopen sets

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

def IsClopen {α : Type u} [TopologicalSpace α] (s : Set α) : Prop

A set is clopen if it is both open and closed.

Equations

• IsClopen s = (IsOpen s ∧ IsClosed s)

theorem IsClopen.isOpen {α : Type u} [TopologicalSpace α] {s : Set α} (hs : IsClopen s) : IsOpen s

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

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

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

Alias of the forward direction of isClopen_iff_frontier_eq_empty.

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

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

@[simp]

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

@[simp]

theorem isClopen_univ {α : Type u} [TopologicalSpace α] : IsClopen Set.univ

theorem IsClopen.compl {α : Type u} [TopologicalSpace α] {s : Set α} (hs : IsClopen s) : IsClopen sᶜ

@[simp]

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

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

theorem IsClopen.prod {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {t : Set β} (hs : IsClopen s) (ht : IsClopen t) : IsClopen (s ×ˢ t)

theorem isClopen_iUnion_of_finite {α : Type u} [TopologicalSpace α] {β : Type u_3} [Finite β] {s : β → Set α} (h : ∀ (i : β), IsClopen (s i)) : IsClopen (⋃ i, s i)

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

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

theorem isClopen_iInter_of_finite {α : Type u} [TopologicalSpace α] {β : Type u_3} [Finite β] {s : β → Set α} (h : ∀ (i : β), IsClopen (s i)) : IsClopen (⋂ i, s i)

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

theorem isClopen_biInter_finset {α : Type u} [TopologicalSpace α] {β : Type u_3} {s : Finset β} {f : β → Set α} (h : ∀ (i : β), i ∈ s → IsClopen (f i)) : IsClopen (⋂ i ∈ s, f i)

theorem IsClopen.preimage {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {s : Set β} (h : IsClopen s) {f : α → β} (hf : Continuous f) : IsClopen (f ⁻¹' s)

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

theorem isClopen_inter_of_disjoint_cover_clopen {α : Type u} [TopologicalSpace α] {Z : Set α} {a : Set α} {b : Set α} (h : IsClopen Z) (cover : Z ⊆ a ∪ b) (ha : IsOpen a) (hb : IsOpen b) (hab : Disjoint a b) : IsClopen (Z ∩ a)

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

@[simp]

theorem isClopen_discrete {α : Type u} [TopologicalSpace α] [DiscreteTopology α] (x : Set α) : IsClopen x

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

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

theorem isClopen_range_sigmaMk {ι : Type u_3} {σ : ι → Type u_4} [(i : ι) → TopologicalSpace (σ i)] {i : ι} : IsClopen (Set.range (Sigma.mk i))

theorem QuotientMap.isClopen_preimage {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : QuotientMap f) {s : Set β} : IsClopen (f ⁻¹' s) ↔ IsClopen s

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

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