mathlib docs: topology.subset

def is_compact {α : Type u} [topological_space α] :

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

is_compact s = ∀ ⦃f : filter α⦄ [_inst_2 : f.ne_bot], f ≤ filter.principal s → (∃ (a : α) (H : a ∈ s), cluster_pt a f)

source

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

(∀ (a : α), a ∈ s → sᶜ ∈ nhds 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.

source

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

(∀ (a : α), a ∈ s → (∃ (t : set α) (H : t ∈ nhds_within a s), 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.

source

theorem is_compact.induction_on {α : Type u} [topological_space α] {s : set α} (hs : is_compact s) {p : set α → Prop} :

p ∅ → (∀ ⦃s t : set α⦄, s ⊆ t → p t → p s) → (∀ ⦃s t : set α⦄, p s → p t → p (s ∪ t)) → (∀ (x : α), x ∈ s → (∃ (t : set α) (H : t ∈ nhds_within x s), p t)) → p s

If p : set α → Prop is stable under restriction and union, and each point x of a compact setshas a neighborhoodtwithinssuch thatp t, thenp s` holds.

source

theorem is_compact.inter_right {α : Type u} [topological_space α] {s t : set α} :

is_compact s → is_closed t → is_compact (s ∩ t)

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

source

theorem is_compact.inter_left {α : Type u} [topological_space α] {s t : set α} :

is_compact t → is_closed s → is_compact (s ∩ t)

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

source

theorem compact_diff {α : Type u} [topological_space α] {s t : set α} :

is_compact s → is_open t → is_compact (s \ t)

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

source

theorem compact_of_is_closed_subset {α : Type u} [topological_space α] {s t : set α} :

is_compact s → is_closed t → t ⊆ s → is_compact t

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

source

theorem is_compact.adherence_nhdset {α : Type u} [topological_space α] {s t : set α} {f : filter α} :

is_compact s → f ≤ filter.principal s → is_open t → (∀ (a : α), a ∈ s → cluster_pt a f → a ∈ t) → t ∈ f

source

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

is_compact s ↔ ∀ (f : filter α), f.is_ultrafilter → f ≤ filter.principal s → (∃ (a : α) (H : a ∈ s), f ≤ nhds a)

source

theorem is_compact.elim_finite_subcover {α : Type u} [topological_space α] {s : set α} {ι : Type v} (hs : is_compact s) (U : ι → set α) :

(∀ (i : ι), is_open (U i)) → (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.

source

theorem is_compact.elim_finite_subfamily_closed {α : Type u} [topological_space α] {s : set α} {ι : Type v} (hs : is_compact s) (Z : ι → set α) :

(∀ (i : ι), is_closed (Z i)) → (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.

source

theorem is_compact.inter_Inter_nonempty {α : Type u} [topological_space α] {s : set α} {ι : Type v} (hs : is_compact s) (Z : ι → set α) :

(∀ (i : ι), is_closed (Z i)) → (∀ (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.

source

theorem is_compact.nonempty_Inter_of_directed_nonempty_compact_closed {α : Type u} [topological_space α] {ι : Type v} [hι : nonempty ι] (Z : ι → set α) :

directed superset Z → (∀ (i : ι), (Z i).nonempty) → (∀ (i : ι), is_compact (Z i)) → (∀ (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.

source

theorem is_compact.nonempty_Inter_of_sequence_nonempty_compact_closed {α : Type u} [topological_space α] (Z : ℕ → set α) :

(∀ (i : ℕ), Z (i + 1) ⊆ Z i) → (∀ (i : ℕ), (Z i).nonempty) → is_compact (Z 0) → (∀ (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.

source

theorem is_compact.elim_finite_subcover_image {α : Type u} {β : Type v} [topological_space α] {s : set α} {b : set β} {c : β → set α} :

is_compact s → (∀ (i : β), i ∈ b → is_open (c i)) → (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.

source

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

(∀ {ι : Type u} (Z : ι → set α), (∀ (i : ι), is_closed (Z i)) → (s ∩ ⋂ (i : ι), Z i) = ∅ → (∃ (t : finset ι), (s ∩ ⋂ (i : ι) (H : i ∈ t), Z i) = ∅)) → is_compact s

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.

source

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

(∀ {ι : Type u} (U : ι → set α), (∀ (i : ι), is_open (U i)) → (s ⊆ ⋃ (i : ι), U i) → (∃ (t : finset ι), s ⊆ ⋃ (i : ι) (H : i ∈ t), U i)) → is_compact s

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

source

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.

source

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.

source

@[simp]

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

is_compact ∅

source

@[simp]

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

is_compact {a}

source

theorem set.finite.compact_bUnion {α : Type u} {β : Type v} [topological_space α] {s : set β} {f : β → set α} :

s.finite → (∀ (i : β), i ∈ s → is_compact (f i)) → is_compact (⋃ (i : β) (H : i ∈ s), f i)

source

theorem compact_Union {α : Type u} {β : Type v} [topological_space α] {f : β → set α} [fintype β] :

(∀ (i : β), is_compact (f i)) → is_compact (⋃ (i : β), f i)

source

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

s.finite → is_compact s

source

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

is_compact s → is_compact t → is_compact (s ∪ t)

source

def nhds_contain_boxes {α : Type u} {β : Type v} [topological_space α] [topological_space β] :

set α → 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

nhds_contain_boxes s t = ∀ (n : set (α × β)), is_open n → s.prod t ⊆ n → (∃ (u : set α) (v : set β), is_open u ∧ is_open v ∧ s ⊆ u ∧ t ⊆ v ∧ u.prod v ⊆ n)

source

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

nhds_contain_boxes s t → nhds_contain_boxes t s

source

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

nhds_contain_boxes s t ↔ nhds_contain_boxes t s

source

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

nhds_contain_boxes {x} {y}

source

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

(∀ (x : α), x ∈ s → nhds_contain_boxes {x} t) → nhds_contain_boxes s t

source

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 (α × β)} :

is_open n → s.prod t ⊆ n → (∃ (u : set α) (v : set β), is_open u ∧ is_open v ∧ s ⊆ u ∧ t ⊆ v ∧ u.prod v ⊆ n)

source

@[class]

structure compact_space (α : Type u_1) [topological_space α] :

Prop

compact_univ : is_compact set.univ

Type class for compact spaces. Separation is sometimes included in the definition, especially in the French literature, but we do not include it here.

Instances

source

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

is_compact set.univ

source

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

∃ (x : α), cluster_pt x f

source

theorem compact_space_of_finite_subfamily_closed {α : Type u} [topological_space α] :

(∀ {ι : Type u} (Z : ι → set α), (∀ (i : ι), is_closed (Z i)) → (⋂ (i : ι), Z i) = ∅ → (∃ (t : finset ι), (⋂ (i : ι) (H : i ∈ t), Z i) = ∅)) → compact_space α

source

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

is_closed s → is_compact s

source

theorem is_compact.image_of_continuous_on {α : Type u} {β : Type v} [topological_space α] {s : set α} [topological_space β] {f : α → β} :

is_compact s → continuous_on f s → is_compact (f '' s)

source

theorem is_compact.image {α : Type u} {β : Type v} [topological_space α] {s : set α} [topological_space β] {f : α → β} :

is_compact s → continuous f → is_compact (f '' s)

source

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

continuous f → is_compact (set.range f)

source

theorem is_closed_proj_of_compact {X : Type u_1} [topological_space X] [compact_space X] {Y : Type u_2} [topological_space Y] :

is_closed_map prod.snd

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

source

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

embedding f → (is_compact s ↔ is_compact (f '' s))

source

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

is_compact s ↔ is_compact (coe '' s)

source

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

is_compact s ↔ is_compact set.univ

source

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

is_compact s ↔ compact_space ↥s

source

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

is_compact s → is_compact t → is_compact (s.prod t)

source

@[instance]

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

compact_space α

Finite topological spaces are compact.

Equations

fintype.compact_space = _

source

@[instance]

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

compact_space (α × β)

The product of two compact spaces is compact.

Equations

prod.compact_space = _

source

@[instance]

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

compact_space (α ⊕ β)

The disjoint union of two compact spaces is compact.

Equations

sum.compact_space = _

source

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

source

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

(∀ (i : ι), is_compact (s i)) → is_compact (set.univ.pi s)

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

source

@[instance]

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

compact_space (Π (i : ι), π i)

Equations

pi.compact = _

source

@[instance]

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

compact_space (quot r)

Equations

quot.compact_space = _

source

@[instance]

def quotient.compact_space {α : Type u} [topological_space α] {s : setoid α} [compact_space α] :

compact_space (quotient s)

Equations

quotient.compact_space = quot.compact_space

source

@[class]

structure locally_compact_space (α : Type u_1) [topological_space α] :

Prop

local_compact_nhds : ∀ (x : α) (n : set α), n ∈ nhds x → (∃ (s : set α) (H : s ∈ nhds x), s ⊆ n ∧ is_compact s)

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

source

theorem exists_compact_subset {α : Type u} [topological_space α] [locally_compact_space α] {x : α} {U : set α} :

is_open U → 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.

source

def is_clopen {α : Type u} [topological_space α] :

set α → Prop

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

Equations

is_clopen s = (is_open s ∧ is_closed s)

source

theorem is_clopen_union {α : Type u} [topological_space α] {s t : set α} :

is_clopen s → is_clopen t → is_clopen (s ∪ t)

source

theorem is_clopen_inter {α : Type u} [topological_space α] {s t : set α} :

is_clopen s → is_clopen t → is_clopen (s ∩ t)

source

@[simp]

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

is_clopen ∅

source

@[simp]

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

is_clopen set.univ

source

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

is_clopen s → is_clopen sᶜ

source

@[simp]

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

is_clopen sᶜ ↔ is_clopen s

source

theorem is_clopen_diff {α : Type u} [topological_space α] {s t : set α} :

is_clopen s → is_clopen t → is_clopen (s \ t)

source

def is_preirreducible {α : Type u} [topological_space α] :

set α → Prop

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

Equations

is_preirreducible s = ∀ (u v : set α), is_open u → is_open v → (s ∩ u).nonempty → (s ∩ v).nonempty → (s ∩ (u ∩ v)).nonempty

source

def is_irreducible {α : Type u} [topological_space α] :

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

is_irreducible s = (s.nonempty ∧ is_preirreducible s)

source

theorem is_irreducible.nonempty {α : Type u} [topological_space α] {s : set α} :

is_irreducible s → s.nonempty

source

theorem is_irreducible.is_preirreducible {α : Type u} [topological_space α] {s : set α} :

is_irreducible s → is_preirreducible s

source

theorem is_preirreducible_empty {α : Type u} [topological_space α] :

is_preirreducible ∅

source

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

is_irreducible {x}

source

theorem is_preirreducible.closure {α : Type u} [topological_space α] {s : set α} :

is_preirreducible s → is_preirreducible (closure s)

source

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

is_irreducible s → is_irreducible (closure s)

source

theorem exists_preirreducible {α : Type u} [topological_space α] (s : set α) :

is_preirreducible s → (∃ (t : set α), is_preirreducible t ∧ s ⊆ t ∧ ∀ (u : set α), is_preirreducible u → t ⊆ u → u = t)

source

def irreducible_component {α : Type u} [topological_space α] :

α → set α

A maximal irreducible set that contains a given point.

Equations

irreducible_component x = classical.some _

source

theorem irreducible_component_property {α : Type u} [topological_space α] (x : α) :

is_preirreducible (irreducible_component x) ∧ {x} ⊆ irreducible_component x ∧ ∀ (u : set α), is_preirreducible u → irreducible_component x ⊆ u → u = irreducible_component x

source

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

x ∈ irreducible_component x

source

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

is_irreducible (irreducible_component x)

source

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

is_preirreducible s → irreducible_component x ⊆ s → s = irreducible_component x

source

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

is_closed (irreducible_component x)

source

@[class]

structure preirreducible_space (α : Type u) [topological_space α] :

Prop

is_preirreducible_univ : is_preirreducible set.univ

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

Instances

irreducible_space.to_preirreducible_space

source

@[class]

structure irreducible_space (α : Type u) [topological_space α] :

Prop

to_preirreducible_space : preirreducible_space α
to_nonempty : nonempty α

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

source

theorem nonempty_preirreducible_inter {α : Type u} [topological_space α] [preirreducible_space α] {s t : set α} :

is_open s → is_open t → s.nonempty → t.nonempty → (s ∩ t).nonempty

source

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

continuous_on f s → is_preirreducible (f '' s)

source

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

continuous_on f s → is_irreducible (f '' s)

source

theorem subtype.preirreducible_space {α : Type u} [topological_space α] {s : set α} :

is_preirreducible s → preirreducible_space ↥s

source

theorem subtype.irreducible_space {α : Type u} [topological_space α] {s : set α} :

is_irreducible s → irreducible_space ↥s

source

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

is_irreducible s ↔ ∀ (U : finset (set α)), (∀ (u : set α), u ∈ U → is_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).

source

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.

source

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

is_irreducible s ↔ ∀ (Z : finset (set α)), (∀ (z : set α), z ∈ Z → is_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.

source

def is_preconnected {α : Type u} [topological_space α] :

set α → Prop

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

Equations

is_preconnected s = ∀ (u v : set α), is_open u → is_open v → s ⊆ u ∪ v → (s ∩ u).nonempty → (s ∩ v).nonempty → (s ∩ (u ∩ v)).nonempty

source

def is_connected {α : Type u} [topological_space α] :

set α → Prop

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

Equations

is_connected s = (s.nonempty ∧ is_preconnected s)

source

theorem is_connected.nonempty {α : Type u} [topological_space α] {s : set α} :

is_connected s → s.nonempty

source

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

is_connected s → is_preconnected s

source

theorem is_preirreducible.is_preconnected {α : Type u} [topological_space α] {s : set α} :

is_preirreducible s → is_preconnected s

source

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

is_irreducible s → is_connected s

source

theorem is_preconnected_empty {α : Type u} [topological_space α] :

is_preconnected ∅

source

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

is_connected {x}

source

theorem is_preconnected_of_forall {α : Type u} [topological_space α] {s : set α} (x : α) :

(∀ (y : α), y ∈ s → (∃ (t : set α) (H : t ⊆ s), x ∈ t ∧ y ∈ t ∧ is_preconnected t)) → is_preconnected s

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

source

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

(∀ (x y : α), x ∈ s → y ∈ s → (∃ (t : set α) (H : t ⊆ s), x ∈ t ∧ y ∈ t ∧ is_preconnected t)) → is_preconnected s

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

source

theorem is_preconnected_sUnion {α : Type u} [topological_space α] (x : α) (c : set (set α)) :

(∀ (s : set α), s ∈ c → x ∈ s) → (∀ (s : set α), s ∈ c → is_preconnected s) → is_preconnected (⋃₀c)

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

source

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

x ∈ s → x ∈ t → is_preconnected s → is_preconnected t → is_preconnected (s ∪ t)

source

theorem is_connected.union {α : Type u} [topological_space α] {s t : set α} :

(s ∩ t).nonempty → is_connected s → is_connected t → is_connected (s ∪ t)

source

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

is_preconnected s → is_preconnected (closure s)

source

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

is_connected s → is_connected (closure s)

source

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

continuous_on f s → is_preconnected (f '' s)

source

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

continuous_on f s → is_connected (f '' s)

source

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

is_preconnected s ↔ ∀ (t t' : set α), is_closed t → is_closed t' → s ⊆ t ∪ t' → (s ∩ t).nonempty → (s ∩ t').nonempty → (s ∩ (t ∩ t')).nonempty

source

def connected_component {α : Type u} [topological_space α] :

α → set α

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

Equations

connected_component x = ⋃₀{s : set α | is_preconnected s ∧ x ∈ s}

source

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

↥F → set α

The connected component of a point inside a set.

Equations

connected_component_in F x = coe '' connected_component x

source

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

x ∈ connected_component x

source

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

is_connected (connected_component x)

source

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

is_preconnected s → x ∈ s → s ⊆ connected_component x

source

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

is_closed (connected_component x)

source

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

irreducible_component x ⊆ connected_component x

source

@[class]

structure preconnected_space (α : Type u) [topological_space α] :

Prop

is_preconnected_univ : is_preconnected set.univ

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

Instances

source

@[class]

structure connected_space (α : Type u) [topological_space α] :

Prop

to_preconnected_space : preconnected_space α
to_nonempty : nonempty α

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

Instances

source

theorem is_connected_range {α : Type u} {β : Type v} [topological_space α] [topological_space β] [connected_space α] {f : α → β} :

continuous f → is_connected (set.range f)

source

theorem connected_space_iff_connected_component {α : Type u} [topological_space α] :

connected_space α ↔ ∃ (x : α), connected_component x = set.univ

source

@[instance]

def preirreducible_space.preconnected_space (α : Type u) [topological_space α] [preirreducible_space α] :

preconnected_space α

Equations

_ = _

source

@[instance]

def irreducible_space.connected_space (α : Type u) [topological_space α] [irreducible_space α] :

connected_space α

Equations

_ = _

source

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

is_open s → is_open t → s ∪ t = set.univ → s.nonempty → t.nonempty → (s ∩ t).nonempty

source

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

is_clopen s ↔ s = ∅ ∨ s = set.univ

source

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

s.nonempty → is_clopen s → s = set.univ

source

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

is_preconnected s → preconnected_space ↥s

source

theorem subtype.connected_space {α : Type u} [topological_space α] {s : set α} :

is_connected s → connected_space ↥s

source

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

is_preconnected s ↔ preconnected_space ↥s

source

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

is_connected s ↔ connected_space ↥s

source

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

is_preconnected s ↔ ∀ (u v : set α), is_open u → is_open v → s ⊆ u ∪ v → s ∩ (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.

source

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

is_connected s ↔ ∀ (U : finset (set α)), (∀ (u v : set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).nonempty → u = v) → (∀ (u : set α), u ∈ U → is_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.

source

def is_totally_disconnected {α : Type u} [topological_space α] :

set α → Prop

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

Equations