mathlib documentation

topology.subset_properties

Properties of subsets of topological spaces

In this file we define various properties of subsets of a topological space, and some classes on topological spaces.

Main definitions

We define the following properties for sets in a topological space:

For each of these definitions (except for is_clopen), we also have a class stating that the whole space satisfies that property: compact_space, irreducible_space, connected_space, totally_disconnected_space, totally_separated_space.

Furthermore, we have two more classes:

On the definition of irreducible and connected sets/spaces

In informal mathematics, irreducible and connected spaces are assumed to be nonempty. We formalise the predicate without that assumption as is_preirreducible and is_preconnected respectively. In other words, the only difference is whether the empty space counts as irreducible and/or connected. There are good reasons to consider the empty space to be “too simple to be simple” See also https://ncatlab.org/nlab/show/too+simple+to+be+simple, and in particular https://ncatlab.org/nlab/show/too+simple+to+be+simple#relationship_to_biased_definitions.

def is_compact {α : Type u} [topological_space α] (s : set α) :
Prop

A set s is compact if for every filter f that contains s, every set of f also meets every neighborhood of some a ∈ s.

Equations
theorem is_compact.compl_mem_sets {α : Type u} [topological_space α] {s : set α} (hs : is_compact s) {f : filter α} (hf : ∀ (a : α), a ss 𝓝 a f) :
s f

The complement to a compact set belongs to a filter f if it belongs to each filter 𝓝 a ⊓ f, a ∈ s.

theorem is_compact.compl_mem_sets_of_nhds_within {α : Type u} [topological_space α] {s : set α} (hs : is_compact s) {f : filter α} (hf : ∀ (a : α), a s(∃ (t : set α) (H : t 𝓝[s] a), t f)) :
s f

The complement to a compact set belongs to a filter f if each a ∈ s has a neighborhood t within s such that tᶜ belongs to f.

theorem is_compact.induction_on {α : Type u} [topological_space α] {s : set α} (hs : is_compact s) {p : set α → Prop} (he : p ) (hmono : ∀ ⦃s t : set α⦄, s tp tp s) (hunion : ∀ ⦃s t : set α⦄, p sp tp (s t)) (hnhds : ∀ (x : α), x s(∃ (t : set α) (H : t 𝓝[s] x), p t)) :
p s

If p : set α → Prop is stable under restriction and union, and each point x of a compact set s has a neighborhood t within s such that p t, then p s holds.

theorem is_compact.inter_right {α : Type u} [topological_space α] {s t : set α} (hs : is_compact s) (ht : is_closed t) :

The intersection of a compact set and a closed set is a compact set.

theorem is_compact.inter_left {α : Type u} [topological_space α] {s t : set α} (ht : is_compact t) (hs : is_closed s) :

The intersection of a closed set and a compact set is a compact set.

theorem compact_diff {α : Type u} [topological_space α] {s t : set α} (hs : is_compact s) (ht : is_open t) :

The set difference of a compact set and an open set is a compact set.

theorem compact_of_is_closed_subset {α : Type u} [topological_space α] {s t : set α} (hs : is_compact s) (ht : is_closed t) (h : t s) :

A closed subset of a compact set is a compact set.

theorem is_compact.adherence_nhdset {α : Type u} [topological_space α] {s t : set α} {f : filter α} (hs : is_compact s) (hf₂ : f 𝓟 s) (ht₁ : is_open t) (ht₂ : ∀ (a : α), a scluster_pt a fa t) :
t f

theorem compact_iff_ultrafilter_le_nhds {α : Type u} [topological_space α] {s : set α} :
is_compact s ∀ (f : ultrafilter α), f 𝓟 s(∃ (a : α) (H : a s), f 𝓝 a)

theorem is_compact.ultrafilter_le_nhds {α : Type u} [topological_space α] {s : set α} :
is_compact s∀ (f : ultrafilter α), f 𝓟 s(∃ (a : α) (H : a s), f 𝓝 a)

Alias of compact_iff_ultrafilter_le_nhds.

theorem is_compact.elim_finite_subcover {α : Type u} [topological_space α] {s : set α} {ι : Type v} (hs : is_compact s) (U : ι → set α) (hUo : ∀ (i : ι), is_open (U i)) (hsU : s ⋃ (i : ι), U i) :
∃ (t : finset ι), s ⋃ (i : ι) (H : i t), U i

For every open cover of a compact set, there exists a finite subcover.

theorem is_compact.elim_finite_subfamily_closed {α : Type u} [topological_space α] {s : set α} {ι : Type v} (hs : is_compact s) (Z : ι → set α) (hZc : ∀ (i : ι), is_closed (Z i)) (hsZ : (s ⋂ (i : ι), Z i) = ) :
∃ (t : finset ι), (s ⋂ (i : ι) (H : i t), Z i) =

For every family of closed sets whose intersection avoids a compact set, there exists a finite subfamily whose intersection avoids this compact set.

theorem is_compact.inter_Inter_nonempty {α : Type u} [topological_space α] {s : set α} {ι : Type v} (hs : is_compact s) (Z : ι → set α) (hZc : ∀ (i : ι), is_closed (Z i)) (hsZ : ∀ (t : finset ι), (s ⋂ (i : ι) (H : i t), Z i).nonempty) :
(s ⋂ (i : ι), Z i).nonempty

To show that a compact set intersects the intersection of a family of closed sets, it is sufficient to show that it intersects every finite subfamily.

theorem is_compact.nonempty_Inter_of_directed_nonempty_compact_closed {α : Type u} [topological_space α] {ι : Type v} [hι : nonempty ι] (Z : ι → set α) (hZd : directed superset Z) (hZn : ∀ (i : ι), (Z i).nonempty) (hZc : ∀ (i : ι), is_compact (Z i)) (hZcl : ∀ (i : ι), is_closed (Z i)) :
(⋂ (i : ι), Z i).nonempty

Cantor's intersection theorem: the intersection of a directed family of nonempty compact closed sets is nonempty.

theorem is_compact.nonempty_Inter_of_sequence_nonempty_compact_closed {α : Type u} [topological_space α] (Z : set α) (hZd : ∀ (i : ), Z (i + 1) Z i) (hZn : ∀ (i : ), (Z i).nonempty) (hZ0 : is_compact (Z 0)) (hZcl : ∀ (i : ), is_closed (Z i)) :
(⋂ (i : ), Z i).nonempty

Cantor's intersection theorem for sequences indexed by : the intersection of a decreasing sequence of nonempty compact closed sets is nonempty.

theorem is_compact.elim_finite_subcover_image {α : Type u} {β : Type v} [topological_space α] {s : set α} {b : set β} {c : β → set α} (hs : is_compact s) (hc₁ : ∀ (i : β), i bis_open (c i)) (hc₂ : s ⋃ (i : β) (H : i b), c i) :
∃ (b' : set β) (H : b' b), b'.finite s ⋃ (i : β) (H : i b'), c i

For every open cover of a compact set, there exists a finite subcover.

theorem compact_of_finite_subfamily_closed {α : Type u} [topological_space α] {s : set α} (h : ∀ {ι : Type u} (Z : ι → set α), (∀ (i : ι), is_closed (Z i))(s ⋂ (i : ι), Z i) = (∃ (t : finset ι), (s ⋂ (i : ι) (H : i t), Z i) = )) :

A set s is compact if for every family of closed sets whose intersection avoids s, there exists a finite subfamily whose intersection avoids s.

theorem compact_of_finite_subcover {α : Type u} [topological_space α] {s : set α} (h : ∀ {ι : Type u} (U : ι → set α), (∀ (i : ι), is_open (U i))(s ⋃ (i : ι), U i)(∃ (t : finset ι), s ⋃ (i : ι) (H : i t), U i)) :

A set s is compact if for every open cover of s, there exists a finite subcover.

theorem compact_iff_finite_subcover {α : Type u} [topological_space α] {s : set α} :
is_compact s ∀ {ι : Type u} (U : ι → set α), (∀ (i : ι), is_open (U i))(s ⋃ (i : ι), U i)(∃ (t : finset ι), s ⋃ (i : ι) (H : i t), U i)

A set s is compact if and only if for every open cover of s, there exists a finite subcover.

theorem compact_iff_finite_subfamily_closed {α : Type u} [topological_space α] {s : set α} :
is_compact s ∀ {ι : Type u} (Z : ι → set α), (∀ (i : ι), is_closed (Z i))(s ⋂ (i : ι), Z i) = (∃ (t : finset ι), (s ⋂ (i : ι) (H : i t), Z i) = )

A set s is compact if and only if for every family of closed sets whose intersection avoids s, there exists a finite subfamily whose intersection avoids s.

@[simp]
theorem compact_empty {α : Type u} [topological_space α] :

@[simp]
theorem compact_singleton {α : Type u} [topological_space α] {a : α} :

theorem set.finite.compact_bUnion {α : Type u} {β : Type v} [topological_space α] {s : set β} {f : β → set α} (hs : s.finite) (hf : ∀ (i : β), i sis_compact (f i)) :
is_compact (⋃ (i : β) (H : i s), f i)

theorem compact_Union {α : Type u} {β : Type v} [topological_space α] {f : β → set α} [fintype β] (h : ∀ (i : β), is_compact (f i)) :
is_compact (⋃ (i : β), f i)

theorem set.finite.is_compact {α : Type u} [topological_space α] {s : set α} (hs : s.finite) :

theorem is_compact.union {α : Type u} [topological_space α] {s t : set α} (hs : is_compact s) (ht : is_compact t) :

theorem is_compact.insert {α : Type u} [topological_space α] {s : set α} (hs : is_compact s) (a : α) :

def filter.cocompact (α : Type u_1) [topological_space α] :

filter.cocompact is the filter generated by complements to compact sets.

Equations
theorem filter.mem_cocompact {α : Type u} [topological_space α] {s : set α} :
s filter.cocompact α ∃ (t : set α), is_compact t t s

theorem filter.mem_cocompact' {α : Type u} [topological_space α] {s : set α} :
s filter.cocompact α ∃ (t : set α), is_compact t s t

theorem is_compact.compl_mem_cocompact {α : Type u} [topological_space α] {s : set α} (hs : is_compact s) :

def nhds_contain_boxes {α : Type u} {β : Type v} [topological_space α] [topological_space β] (s : set α) (t : set β) :
Prop

nhds_contain_boxes s t means that any open neighborhood of s × t in α × β includes a product of an open neighborhood of s by an open neighborhood of t.

Equations
theorem nhds_contain_boxes.symm {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set α} {t : set β} :

theorem nhds_contain_boxes.comm {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set α} {t : set β} :

theorem nhds_contain_boxes_of_singleton {α : Type u} {β : Type v} [topological_space α] [topological_space β] {x : α} {y : β} :

theorem nhds_contain_boxes_of_compact {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set α} (hs : is_compact s) (t : set β) (H : ∀ (x : α), x snhds_contain_boxes {x} t) :

theorem generalized_tube_lemma {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set α} (hs : is_compact s) {t : set β} (ht : is_compact t) {n : set × β)} (hn : is_open n) (hp : s.prod t n) :
∃ (u : set α) (v : set β), is_open u is_open v s u t v u.prod v n

If s and t are compact sets and n is an open neighborhood of s × t, then there exist open neighborhoods u ⊇ s and v ⊇ t such that u × v ⊆ n.

theorem compact_univ {α : Type u} [topological_space α] [h : compact_space α] :

theorem cluster_point_of_compact {α : Type u} [topological_space α] [compact_space α] (f : filter α) [f.ne_bot] :
∃ (x : α), cluster_pt x f

theorem compact_space_of_finite_subfamily_closed {α : Type u} [topological_space α] (h : ∀ {ι : Type u} (Z : ι → set α), (∀ (i : ι), is_closed (Z i))(⋂ (i : ι), Z i) = (∃ (t : finset ι), (⋂ (i : ι) (H : i t), Z i) = )) :

theorem is_closed.compact {α : Type u} [topological_space α] [compact_space α] {s : set α} (h : is_closed s) :

theorem is_compact.image_of_continuous_on {α : Type u} {β : Type v} [topological_space α] {s : set α} [topological_space β] {f : α → β} (hs : is_compact s) (hf : continuous_on f s) :

theorem is_compact.image {α : Type u} {β : Type v} [topological_space α] {s : set α} [topological_space β] {f : α → β} (hs : is_compact s) (hf : continuous f) :

theorem compact_range {α : Type u} {β : Type v} [topological_space α] [topological_space β] [compact_space α] {f : α → β} (hf : continuous f) :

If X is is_compact then pr₂ : X × Y → Y is a closed map

theorem embedding.compact_iff_compact_image {α : Type u} {β : Type v} [topological_space α] {s : set α} [topological_space β] {f : α → β} (hf : embedding f) :

theorem compact_iff_compact_in_subtype {α : Type u} [topological_space α] {p : α → Prop} {s : set {a // p a}} :

theorem is_compact.prod {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set α} {t : set β} (hs : is_compact s) (ht : is_compact t) :

@[instance]
def fintype.compact_space {α : Type u} [topological_space α] [fintype α] :

Finite topological spaces are compact.

@[instance]
def prod.compact_space {α : Type u} {β : Type v} [topological_space α] [topological_space β] [compact_space α] [compact_space β] :

The product of two compact spaces is compact.

@[instance]
def sum.compact_space {α : Type u} {β : Type v} [topological_space α] [topological_space β] [compact_space α] [compact_space β] :

The disjoint union of two compact spaces is compact.

theorem compact_pi_infinite {ι : Type u_1} {π : ι → Type u_2} [Π (i : ι), topological_space («π» i)] {s : Π (i : ι), set («π» i)} :
(∀ (i : ι), is_compact (s i))is_compact {x : Π (i : ι), «π» i | ∀ (i : ι), x i s i}

Tychonoff's theorem

theorem compact_univ_pi {ι : Type u_1} {π : ι → Type u_2} [Π (i : ι), topological_space («π» i)] {s : Π (i : ι), set («π» i)} (h : ∀ (i : ι), is_compact (s i)) :

A version of Tychonoff's theorem that uses set.pi.

@[instance]
def pi.compact {ι : Type u_1} {π : ι → Type u_2} [Π (i : ι), topological_space («π» i)] [∀ (i : ι), compact_space («π» i)] :
compact_space (Π (i : ι), «π» i)

@[instance]
def quot.compact_space {α : Type u} [topological_space α] {r : α → α → Prop} [compact_space α] :
compact_space (quot r)

@[instance]

@[class]
structure locally_compact_space (α : Type u_1) [topological_space α] :
Prop

There are various definitions of "locally compact space" in the literature, which agree for Hausdorff spaces but not in general. This one is the precise condition on X needed for the evaluation map C(X, Y) × X → Y to be continuous for all Y when C(X, Y) is given the compact-open topology.

Instances
theorem exists_compact_subset {α : Type u} [topological_space α] [locally_compact_space α] {x : α} {U : set α} (hU : is_open U) (hx : x U) :
∃ (K : set α), is_compact K x interior K K U

A reformulation of the definition of locally compact space: In a locally compact space, every open set containing x has a compact subset containing x in its interior.

theorem ultrafilter.le_nhds_Lim {α : Type u} [topological_space α] [compact_space α] (F : ultrafilter α) :

@[class]
structure sigma_compact_space (α : Type u_1) [topological_space α] :
Prop

A σ-compact space is a space that is the union of a countable collection of compact subspaces. Note that a locally compact separable T₂ space need not be σ-compact. The sequence can be extracted using topological_space.compact_covering.

Instances
def compact_covering (α : Type u) [topological_space α] [sigma_compact_space α] :
set α

An arbitrary compact covering of a σ-compact space.

Equations
theorem Union_compact_covering (α : Type u) [topological_space α] [sigma_compact_space α] :
(⋃ (n : ), compact_covering α n) = set.univ

def is_clopen {α : Type u} [topological_space α] (s : set α) :
Prop

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

Equations
theorem is_clopen_union {α : Type u} [topological_space α] {s t : set α} (hs : is_clopen s) (ht : is_clopen t) :

theorem is_clopen_inter {α : Type u} [topological_space α] {s t : set α} (hs : is_clopen s) (ht : is_clopen t) :

@[simp]
theorem is_clopen_empty {α : Type u} [topological_space α] :

@[simp]
theorem is_clopen_univ {α : Type u} [topological_space α] :

theorem is_clopen_compl {α : Type u} [topological_space α] {s : set α} (hs : is_clopen s) :

@[simp]
theorem is_clopen_compl_iff {α : Type u} [topological_space α] {s : set α} :

theorem is_clopen_diff {α : Type u} [topological_space α] {s t : set α} (hs : is_clopen s) (ht : is_clopen t) :
is_clopen (s \ t)

theorem is_clopen_Inter {α : Type u} [topological_space α] {β : Type u_1} [fintype β] {s : β → set α} (h : ∀ (i : β), is_clopen (s i)) :
is_clopen (⋂ (i : β), s i)

theorem is_clopen_bInter {α : Type u} [topological_space α] {β : Type u_1} {s : finset β} {f : β → set α} (h : ∀ (i : β), i sis_clopen (f i)) :
is_clopen (⋂ (i : β) (H : i s), f i)

theorem continuous_on.preimage_clopen_of_clopen {α : Type u} [topological_space α] {β : Type u_1} [topological_space β] {f : α → β} {s : set α} {t : set β} (hf : continuous_on f s) (hs : is_clopen s) (ht : is_clopen t) :

theorem is_clopen_inter_of_disjoint_cover_clopen {α : Type u} [topological_space α] {Z a b : set α} (h : is_clopen Z) (cover : Z a b) (ha : is_open a) (hb : is_open b) (hab : a b = ) :

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

def is_preirreducible {α : Type u} [topological_space α] (s : set α) :
Prop

A preirreducible set s is one where there is no non-trivial pair of disjoint opens on s.

Equations
def is_irreducible {α : Type u} [topological_space α] (s : set α) :
Prop

An irreducible set s is one that is nonempty and where there is no non-trivial pair of disjoint opens on s.

Equations
theorem is_irreducible.nonempty {α : Type u} [topological_space α] {s : set α} (h : is_irreducible s) :

theorem is_irreducible_singleton {α : Type u} [topological_space α] {x : α} :

theorem is_irreducible.closure {α : Type u} [topological_space α] {s : set α} (h : is_irreducible s) :

theorem exists_preirreducible {α : Type u} [topological_space α] (s : set α) (H : is_preirreducible s) :
∃ (t : set α), is_preirreducible t s t ∀ (u : set α), is_preirreducible ut uu = t

def irreducible_component {α : Type u} [topological_space α] (x : α) :
set α

A maximal irreducible set that contains a given point.

Equations
theorem mem_irreducible_component {α : Type u} [topological_space α] {x : α} :

theorem eq_irreducible_component {α : Type u} [topological_space α] {x : α} {s : set α} :

@[class]
structure preirreducible_space (α : Type u) [topological_space α] :
Prop

A preirreducible space is one where there is no non-trivial pair of disjoint opens.

Instances
@[class]
structure irreducible_space (α : Type u) [topological_space α] :
Prop

An irreducible space is one that is nonempty and where there is no non-trivial pair of disjoint opens.

theorem nonempty_preirreducible_inter {α : Type u} [topological_space α] [preirreducible_space α] {s t : set α} :
is_open sis_open ts.nonemptyt.nonempty(s t).nonempty

theorem is_preirreducible.image {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set α} (H : is_preirreducible s) (f : α → β) (hf : continuous_on f s) :

theorem is_irreducible.image {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set α} (H : is_irreducible s) (f : α → β) (hf : continuous_on f s) :

theorem is_irreducible_iff_sInter {α : Type u} [topological_space α] {s : set α} :
is_irreducible s ∀ (U : finset (set α)), (∀ (u : set α), u Uis_open u)(∀ (u : set α), u U(s u).nonempty)(s ⋂₀U).nonempty

A set s is irreducible if and only if for every finite collection of open sets all of whose members intersect s, s also intersects the intersection of the entire collection (i.e., there is an element of s contained in every member of the collection).

theorem is_preirreducible_iff_closed_union_closed {α : Type u} [topological_space α] {s : set α} :
is_preirreducible s ∀ (z₁ z₂ : set α), is_closed z₁is_closed z₂s z₁ z₂s z₁ s z₂

A set is preirreducible if and only if for every cover by two closed sets, it is contained in one of the two covering sets.

theorem is_irreducible_iff_sUnion_closed {α : Type u} [topological_space α] {s : set α} :
is_irreducible s ∀ (Z : finset (set α)), (∀ (z : set α), z Zis_closed z)s ⋃₀Z(∃ (z : set α) (H : z Z), s z)

A set is irreducible if and only if for every cover by a finite collection of closed sets, it is contained in one of the members of the collection.

def is_preconnected {α : Type u} [topological_space α] (s : set α) :
Prop

A preconnected set is one where there is no non-trivial open partition.

Equations
def is_connected {α : Type u} [topological_space α] (s : set α) :
Prop

A connected set is one that is nonempty and where there is no non-trivial open partition.

Equations
theorem is_connected.nonempty {α : Type u} [topological_space α] {s : set α} (h : is_connected s) :

theorem is_connected.is_preconnected {α : Type u} [topological_space α] {s : set α} (h : is_connected s) :

theorem is_irreducible.is_connected {α : Type u} [topological_space α] {s : set α} (H : is_irreducible s) :

theorem is_connected_singleton {α : Type u} [topological_space α] {x : α} :

theorem is_preconnected_of_forall {α : Type u} [topological_space α] {s : set α} (x : α) (H : ∀ (y : α), y s(∃ (t : set α) (H : t s), x t y t is_preconnected t)) :

If any point of a set is joined to a fixed point by a preconnected subset, then the original set is preconnected as well.

theorem is_preconnected_of_forall_pair {α : Type u} [topological_space α] {s : set α} (H : ∀ (x y : α), x sy s(∃ (t : set α) (H : t s), x t y t is_preconnected t)) :

If any two points of a set are contained in a preconnected subset, then the original set is preconnected as well.

theorem is_preconnected_sUnion {α : Type u} [topological_space α] (x : α) (c : set (set α)) (H1 : ∀ (s : set α), s cx s) (H2 : ∀ (s : set α), s cis_preconnected s) :

A union of a family of preconnected sets with a common point is preconnected as well.

theorem is_preconnected.union {α : Type u} [topological_space α] (x : α) {s t : set α} (H1 : x s) (H2 : x t) (H3 : is_preconnected s) (H4 : is_preconnected t) :

theorem is_connected.union {α : Type u} [topological_space α] {s t : set α} (H : (s t).nonempty) (Hs : is_connected s) (Ht : is_connected t) :

theorem is_preconnected.closure {α : Type u} [topological_space α] {s : set α} (H : is_preconnected s) :

theorem is_connected.closure {α : Type u} [topological_space α] {s : set α} (H : is_connected s) :

theorem is_preconnected.image {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set α} (H : is_preconnected s) (f : α → β) (hf : continuous_on f s) :

theorem is_connected.image {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set α} (H : is_connected s) (f : α → β) (hf : continuous_on f s) :

theorem is_preconnected_closed_iff {α : Type u} [topological_space α] {s : set α} :
is_preconnected s ∀ (t t' : set α), is_closed tis_closed t's t t'(s t).nonempty(s t').nonempty(s (t t')).nonempty

def connected_component {α : Type u} [topological_space α] (x : α) :
set α

The connected component of a point is the maximal connected set that contains this point.

Equations
def connected_component_in {α : Type u} [topological_space α] (F : set α) (x : F) :
set α

The connected component of a point inside a set.

Equations
theorem mem_connected_component {α : Type u} [topological_space α] {x : α} :

theorem subset_connected_component {α : Type u} [topological_space α] {x : α} {s : set α} (H1 : is_preconnected s) (H2 : x s) :

@[class]
structure preconnected_space (α : Type u) [topological_space α] :
Prop

A preconnected space is one where there is no non-trivial open partition.

Instances
@[class]
structure connected_space (α : Type u) [topological_space α] :
Prop

A connected space is a nonempty one where there is no non-trivial open partition.

Instances
theorem is_connected_range {α : Type u} {β : Type v} [topological_space α] [topological_space β] [connected_space α] {f : α → β} (h : continuous f) :

theorem nonempty_inter {α : Type u} [topological_space α] [preconnected_space α] {s t : set α} :
is_open sis_open ts t = set.univs.nonemptyt.nonempty(s t).nonempty

theorem is_clopen_iff {α : Type u} [topological_space α] [preconnected_space α] {s : set α} :

theorem eq_univ_of_nonempty_clopen {α : Type u} [topological_space α] [preconnected_space α] {s : set α} (h : s.nonempty) (h' : is_clopen s) :

theorem subtype.connected_space {α : Type u} [topological_space α] {s : set α} (h : is_connected s) :

theorem is_preconnected_iff_subset_of_disjoint {α : Type u} [topological_space α] {s : set α} :
is_preconnected s ∀ (u v : set α), is_open uis_open vs u vs (u v) = s u s v

A set s is preconnected if and only if for every cover by two open sets that are disjoint on s, it is contained in one of the two covering sets.

theorem is_connected_iff_sUnion_disjoint_open {α : Type u} [topological_space α] {s : set α} :
is_connected s ∀ (U : finset (set α)), (∀ (u v : set α), u Uv U(s (u v)).nonemptyu = v)(∀ (u : set α), u Uis_open u)s ⋃₀U(∃ (u : set α) (H : u U), s u)

A set s is connected if and only if for every cover by a finite collection of open sets that are pairwise disjoint on s, it is contained in one of the members of the collection.

theorem subset_or_disjoint_of_clopen {α : Type u_1} [topological_space α] {s t : set α} (h : is_preconnected t) (h1 : is_clopen s) :
s t = t s

Preconnected sets are either contained in or disjoint to any given clopen set.

theorem is_preconnected_iff_subset_of_disjoint_closed {α : Type u_1} {s : set α} [topological_space α] :
is_preconnected s ∀ (u v : set α), is_closed uis_closed vs u vs (u v) = s u s v

A set s is preconnected if and only if for every cover by two closed sets that are disjoint on s, it is contained in one of the two covering sets.

theorem is_preconnected_iff_subset_of_fully_disjoint_closed {α : Type u} [topological_space α] {s : set α} (hs : is_closed s) :
is_preconnected s ∀ (u v : set α), is_closed uis_closed vs u vu v = s u s v

A closed set s is preconnected if and only if for every cover by two closed sets that are disjoint, it is contained in one of the two covering sets.

theorem connected_component_subset_Inter_clopen {α : Type u} [topological_space α] {x : α} :
connected_component x ⋂ (Z : {Z // is_clopen Z x Z}), Z

The connected component of a point is always a subset of the intersection of all its clopen neighbourhoods.

def is_totally_disconnected {α : Type u} [topological_space α] (s : set α) :
Prop

A set is called totally disconnected if all of its connected components are singletons.

Equations
@[class]
structure totally_disconnected_space (α : Type u) [topological_space α] :
Prop

A space is totally disconnected if all of its connected components are singletons.

Instances
@[instance]
def pi.totally_disconnected_space {α : Type u_1} {β : α → Type u_2} [t₂ : Π (a : α), topological_space (β a)] [∀ (a : α), totally_disconnected_space (β a)] :
totally_disconnected_space (Π (a : α), β a)

def is_totally_separated {α : Type u} [topological_space α] (s : set α) :
Prop

A set s is called totally separated if any two points of this set can be separated by two disjoint open sets covering s.

Equations
@[class]
structure totally_separated_space (α : Type u) [topological_space α] :
Prop

A space is totally separated if any two points can be separated by two disjoint open sets covering the whole space.

Instances