mathlib documentation

topology.order

Ordering on topologies and (co)induced topologies #

Topologies on a fixed type α are ordered, by reverse inclusion. That is, for topologies t₁ and t₂ on α, we write t₁ ≤ t₂ if every set open in t₂ is also open in t₁. (One also calls t₁ finer than t₂, and t₂ coarser than t₁.)

Any function f : α → β induces induced f : topological_space β → topological_space α and coinduced f : topological_space α → topological_space β. Continuity, the ordering on topologies and (co)induced topologies are related as follows:

Topologies on α form a complete lattice, with ⊥ the discrete topology and ⊤ the indiscrete topology.

For a function f : α → β, (coinduced f, induced f) is a Galois connection between topologies on α and topologies on β.

Implementation notes #

There is a Galois insertion between topologies on α (with the inclusion ordering) and all collections of sets in α. The complete lattice structure on topologies on α is defined as the reverse of the one obtained via this Galois insertion.

Tags #

finer, coarser, induced topology, coinduced topology

inductive topological_space.generate_open {α : Type u} (g : set (set α)) :
set α → Prop

The open sets of the least topology containing a collection of basic sets.

def topological_space.generate_from {α : Type u} (g : set (set α)) :

The smallest topological space containing the collection g of basic sets

Equations
theorem topological_space.is_open_generate_from_of_mem {α : Type u} {g : set (set α)} {s : set α} (hs : s g) :
theorem topological_space.nhds_generate_from {α : Type u} {g : set (set α)} {a : α} :
nhds a = ⨅ (s : set α) (H : s {s : set α | a s s g}), filter.principal s
theorem topological_space.tendsto_nhds_generate_from {α : Type u} {β : Type u_1} {m : α → β} {f : filter α} {g : set (set β)} {b : β} (h : ∀ (s : set β), s gb sm ⁻¹' s f) :
@[protected]
def topological_space.mk_of_nhds {α : Type u} (n : α → filter α) :

Construct a topology on α given the filter of neighborhoods of each point of α.

Equations
theorem topological_space.nhds_mk_of_nhds {α : Type u} (n : α → filter α) (a : α) (h₀ : has_pure.pure n) (h₁ : ∀ {a : α} {s : set α}, s n a(∃ (t : set α) (H : t n a), t s ∀ (a' : α), a' ts n a')) :
nhds a = n a
theorem topological_space.nhds_mk_of_nhds_filter_basis {α : Type u} (B : α → filter_basis α) (a : α) (h₀ : ∀ (x : α) (n : set α), n B xx n) (h₁ : ∀ (x : α) (n : set α), n B x(∃ (n₁ : set α) (H : n₁ B x), n₁ n ∀ (x' : α), x' n₁(∃ (n₂ : set α) (H : n₂ B x'), n₂ n))) :
nhds a = (B a).filter
def tmp_order {α : Type u} :

The inclusion ordering on topologies on α. We use it to get a complete lattice instance via the Galois insertion method, but the partial order that we will eventually impose on topological_space α is the reverse one.

Equations
@[protected]
def mk_of_closure {α : Type u} (s : set (set α)) (hs : {u : set α | (topological_space.generate_from s).is_open u} = s) :

If s equals the collection of open sets in the topology it generates, then s defines a topology.

Equations
theorem mk_of_closure_sets {α : Type u} {s : set (set α)} {hs : {u : set α | (topological_space.generate_from s).is_open u} = s} :
def gi_generate_from (α : Type u_1) :

The Galois insertion between set (set α) and topological_space α whose lower part sends a collection of subsets of α to the topology they generate, and whose upper part sends a topology to its collection of open subsets.

Equations
theorem generate_from_mono {α : Type u_1} {g₁ g₂ : set (set α)} (h : g₁ g₂) :
theorem set_of_is_open_injective {α : Type u} :
function.injective (λ (t : topological_space α), {s : set α | t.is_open s})

The "temporary" order tmp_order on topological_space α, i.e. the inclusion order, is a complete lattice. (Note that later topological_space α will equipped with the dual order to tmp_order).

Equations
@[protected, instance]
Equations
@[protected]
theorem topological_space.le_def {α : Type u_1} {t s : topological_space α} :
@[protected, instance]

The ordering on topologies on the type α. t ≤ s if every set open in s is also open in t (t is finer than s).

Equations
theorem le_generate_from_iff_subset_is_open {α : Type u} {g : set (set α)} {t : topological_space α} :
@[protected, instance]

Topologies on α form a complete lattice, with the discrete topology and the indiscrete topology. The infimum of a collection of topologies is the topology generated by all their open sets, while the supremum is the topology whose open sets are those sets open in every member of the collection.

Equations
theorem is_open_implies_is_open_iff {α : Type u} {a b : topological_space α} :
(∀ (s : set α), a.is_open sb.is_open s) b a
@[protected, instance]
def discrete_topology_bot (α : Type u_1) :
@[simp]
theorem is_open_discrete {α : Type u} [topological_space α] [discrete_topology α] (s : set α) :
@[simp]
theorem is_closed_discrete {α : Type u} [topological_space α] [discrete_topology α] (s : set α) :
theorem continuous_of_discrete_topology {α : Type u} {β : Type v} [topological_space α] [discrete_topology α] [topological_space β] {f : α → β} :
theorem nhds_bot (α : Type u_1) :
theorem mem_nhds_discrete {α : Type u} [topological_space α] [discrete_topology α] {x : α} {s : set α} :
s nhds x x s
theorem le_of_nhds_le_nhds {α : Type u} {t₁ t₂ : topological_space α} (h : ∀ (x : α), nhds x nhds x) :
t₁ t₂
theorem eq_of_nhds_eq_nhds {α : Type u} {t₁ t₂ : topological_space α} (h : ∀ (x : α), nhds x = nhds x) :
t₁ = t₂
theorem eq_bot_of_singletons_open {α : Type u} {t : topological_space α} (h : ∀ (x : α), t.is_open {x}) :
t =
theorem forall_open_iff_discrete {X : Type u_1} [topological_space X] :
(∀ (s : set X), is_open s) discrete_topology X
theorem singletons_open_iff_discrete {X : Type u_1} [topological_space X] :
(∀ (a : X), is_open {a}) discrete_topology X
def topological_space.induced {α : Type u} {β : Type v} (f : α → β) (t : topological_space β) :

Given f : α → β and a topology on β, the induced topology on α is the collection of sets that are preimages of some open set in β. This is the coarsest topology that makes f continuous.

Equations
theorem is_open_induced_iff {α : Type u_1} {β : Type u_2} [t : topological_space β] {s : set α} {f : α → β} :
is_open s ∃ (t_1 : set β), is_open t_1 f ⁻¹' t_1 = s
theorem is_open_induced_iff' {α : Type u_1} {β : Type u_2} [t : topological_space β] {s : set α} {f : α → β} :
(topological_space.induced f t).is_open s ∃ (t_1 : set β), is_open t_1 f ⁻¹' t_1 = s
theorem is_closed_induced_iff {α : Type u_1} {β : Type u_2} [t : topological_space β] {s : set α} {f : α → β} :
is_closed s ∃ (t_1 : set β), is_closed t_1 f ⁻¹' t_1 = s
def topological_space.coinduced {α : Type u} {β : Type v} (f : α → β) (t : topological_space α) :

Given f : α → β and a topology on α, the coinduced topology on β is defined such that s:set β is open if the preimage of s is open. This is the finest topology that makes f continuous.

Equations
theorem is_open_coinduced {α : Type u_1} {β : Type u_2} {t : topological_space α} {s : set β} {f : α → β} :
theorem preimage_nhds_coinduced {α : Type u_1} {β : Type u_2} [topological_space α] {π : α → β} {s : set β} {a : α} (hs : s nhds (π a)) :
π ⁻¹' s nhds a
theorem continuous.coinduced_le {α : Type u_1} {β : Type u_2} {t : topological_space α} {t' : topological_space β} {f : α → β} (h : continuous f) :
theorem coinduced_le_iff_le_induced {α : Type u_1} {β : Type u_2} {f : α → β} {tα : topological_space α} {tβ : topological_space β} :
theorem continuous.le_induced {α : Type u_1} {β : Type u_2} {t : topological_space α} {t' : topological_space β} {f : α → β} (h : continuous f) :
theorem gc_coinduced_induced {α : Type u_1} {β : Type u_2} (f : α → β) :
theorem induced_mono {α : Type u_1} {β : Type u_2} {t₁ t₂ : topological_space α} {g : β → α} (h : t₁ t₂) :
theorem coinduced_mono {α : Type u_1} {β : Type u_2} {t₁ t₂ : topological_space α} {f : α → β} (h : t₁ t₂) :
@[simp]
theorem induced_top {α : Type u_1} {β : Type u_2} {g : β → α} :
@[simp]
theorem induced_inf {α : Type u_1} {β : Type u_2} {t₁ t₂ : topological_space α} {g : β → α} :
@[simp]
theorem induced_infi {α : Type u_1} {β : Type u_2} {g : β → α} {ι : Sort w} {t : ι → topological_space α} :
topological_space.induced g (⨅ (i : ι), t i) = ⨅ (i : ι), topological_space.induced g (t i)
@[simp]
theorem coinduced_bot {α : Type u_1} {β : Type u_2} {f : α → β} :
@[simp]
theorem coinduced_sup {α : Type u_1} {β : Type u_2} {t₁ t₂ : topological_space α} {f : α → β} :
@[simp]
theorem coinduced_supr {α : Type u_1} {β : Type u_2} {f : α → β} {ι : Sort w} {t : ι → topological_space α} :
topological_space.coinduced f (⨆ (i : ι), t i) = ⨆ (i : ι), topological_space.coinduced f (t i)
theorem induced_id {α : Type u_1} [t : topological_space α] :
theorem induced_compose {α : Type u_1} {β : Type u_2} {γ : Type u_3} [tγ : topological_space γ] {f : α → β} {g : β → γ} :
theorem induced_const {α : Type u_1} {β : Type u_2} [t : topological_space α] {x : α} :
topological_space.induced (λ (y : β), x) t =
theorem coinduced_id {α : Type u_1} [t : topological_space α] :
theorem coinduced_compose {α : Type u_1} {β : Type u_2} {γ : Type u_3} [tα : topological_space α] {f : α → β} {g : β → γ} :
theorem equiv.induced_symm {α : Type u_1} {β : Type u_2} (e : α β) :
theorem equiv.coinduced_symm {α : Type u_1} {β : Type u_2} (e : α β) :
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
theorem continuous_empty_function {α : Type u} {β : Type v} [topological_space α] [topological_space β] [is_empty β] (f : α → β) :
theorem le_generate_from {α : Type u} {t : topological_space α} {g : set (set α)} (h : ∀ (s : set α), s gis_open s) :
theorem induced_generate_from_eq {α : Type u_1} {β : Type u_2} {b : set (set β)} {f : α → β} :
theorem le_induced_generate_from {α : Type u_1} {β : Type u_2} [t : topological_space α] {b : set (set β)} {f : α → β} (h : ∀ (a : set β), a bis_open (f ⁻¹' a)) :
def nhds_adjoint {α : Type u} (a : α) (f : filter α) :

This construction is left adjoint to the operation sending a topology on α to its neighborhood filter at a fixed point a : α.

Equations
theorem gc_nhds {α : Type u} (a : α) :
theorem nhds_mono {α : Type u} {t₁ t₂ : topological_space α} {a : α} (h : t₁ t₂) :
theorem le_iff_nhds {α : Type u_1} (t t' : topological_space α) :
t t' ∀ (x : α), nhds x nhds x
theorem nhds_adjoint_nhds {α : Type u_1} (a : α) (f : filter α) :
theorem nhds_adjoint_nhds_of_ne {α : Type u_1} (a : α) (f : filter α) {b : α} (h : b a) :
theorem is_open_singleton_nhds_adjoint {α : Type u_1} {a b : α} (f : filter α) (hb : b a) :
theorem le_nhds_adjoint_iff' {α : Type u_1} (a : α) (f : filter α) (t : topological_space α) :
t nhds_adjoint a f nhds a has_pure.pure a f ∀ (b : α), b anhds b = has_pure.pure b
theorem le_nhds_adjoint_iff {α : Type u_1} (a : α) (f : filter α) (t : topological_space α) :
t nhds_adjoint a f nhds a has_pure.pure a f ∀ (b : α), b at.is_open {b}
theorem nhds_infi {α : Type u} {ι : Sort u_1} {t : ι → topological_space α} {a : α} :
nhds a = ⨅ (i : ι), nhds a
theorem nhds_Inf {α : Type u} {s : set (topological_space α)} {a : α} :
nhds a = ⨅ (t : topological_space α) (H : t s), nhds a
theorem nhds_inf {α : Type u} {t₁ t₂ : topological_space α} {a : α} :
theorem nhds_top {α : Type u} {a : α} :
theorem is_open_sup {α : Type u} {t₁ t₂ : topological_space α} {s : set α} :
theorem continuous_iff_coinduced_le {α : Type u} {β : Type v} {f : α → β} {t₁ : topological_space α} {t₂ : topological_space β} :
theorem continuous_iff_le_induced {α : Type u} {β : Type v} {f : α → β} {t₁ : topological_space α} {t₂ : topological_space β} :
theorem continuous_generated_from {α : Type u} {β : Type v} {f : α → β} {t : topological_space α} {b : set (set β)} (h : ∀ (s : set β), s bis_open (f ⁻¹' s)) :
@[continuity]
theorem continuous_induced_dom {α : Type u} {β : Type v} {f : α → β} {t : topological_space β} :
theorem continuous_induced_rng {α : Type u} {β : Type v} {γ : Type u_1} {f : α → β} {g : γ → α} {t₂ : topological_space β} {t₁ : topological_space γ} :
theorem continuous_coinduced_rng {α : Type u} {β : Type v} {f : α → β} {t : topological_space α} :
theorem continuous_coinduced_dom {α : Type u} {β : Type v} {γ : Type u_1} {f : α → β} {g : β → γ} {t₁ : topological_space α} {t₂ : topological_space γ} :
theorem continuous_le_dom {α : Type u} {β : Type v} {f : α → β} {t₁ t₂ : topological_space α} {t₃ : topological_space β} (h₁ : t₂ t₁) (h₂ : continuous f) :
theorem continuous_le_rng {α : Type u} {β : Type v} {f : α → β} {t₁ : topological_space α} {t₂ t₃ : topological_space β} (h₁ : t₂ t₃) (h₂ : continuous f) :
theorem continuous_sup_dom {α : Type u} {β : Type v} {f : α → β} {t₁ t₂ : topological_space α} {t₃ : topological_space β} :
theorem continuous_sup_rng_left {α : Type u} {β : Type v} {f : α → β} {t₁ : topological_space α} {t₃ t₂ : topological_space β} :
theorem continuous_sup_rng_right {α : Type u} {β : Type v} {f : α → β} {t₁ : topological_space α} {t₃ t₂ : topological_space β} :
theorem continuous_Sup_dom {α : Type u} {β : Type v} {f : α → β} {T : set (topological_space α)} {t₂ : topological_space β} :
continuous f ∀ (t : topological_space α), t Tcontinuous f
theorem continuous_Sup_rng {α : Type u} {β : Type v} {f : α → β} {t₁ : topological_space α} {t₂ : set (topological_space β)} {t : topological_space β} (h₁ : t t₂) (hf : continuous f) :
theorem continuous_supr_dom {α : Type u} {β : Type v} {f : α → β} {ι : Sort u_2} {t₁ : ι → topological_space α} {t₂ : topological_space β} :
continuous f ∀ (i : ι), continuous f
theorem continuous_supr_rng {α : Type u} {β : Type v} {f : α → β} {ι : Sort u_2} {t₁ : topological_space α} {t₂ : ι → topological_space β} {i : ι} (h : continuous f) :
theorem continuous_inf_rng {α : Type u} {β : Type v} {f : α → β} {t₁ : topological_space α} {t₂ t₃ : topological_space β} :
theorem continuous_inf_dom_left {α : Type u} {β : Type v} {f : α → β} {t₁ t₂ : topological_space α} {t₃ : topological_space β} :
theorem continuous_inf_dom_right {α : Type u} {β : Type v} {f : α → β} {t₁ t₂ : topological_space α} {t₃ : topological_space β} :
theorem continuous_Inf_dom {α : Type u} {β : Type v} {f : α → β} {t₁ : set (topological_space α)} {t₂ : topological_space β} {t : topological_space α} (h₁ : t t₁) :
theorem continuous_Inf_rng {α : Type u} {β : Type v} {f : α → β} {t₁ : topological_space α} {T : set (topological_space β)} :
continuous f ∀ (t : topological_space β), t Tcontinuous f
theorem continuous_infi_dom {α : Type u} {β : Type v} {f : α → β} {ι : Sort u_2} {t₁ : ι → topological_space α} {t₂ : topological_space β} {i : ι} :
theorem continuous_infi_rng {α : Type u} {β : Type v} {f : α → β} {ι : Sort u_2} {t₁ : topological_space α} {t₂ : ι → topological_space β} :
continuous f ∀ (i : ι), continuous f
@[continuity]
theorem continuous_bot {α : Type u} {β : Type v} {f : α → β} {t : topological_space β} :
@[continuity]
theorem continuous_top {α : Type u} {β : Type v} {f : α → β} {t : topological_space α} :
theorem continuous_id_iff_le {α : Type u} {t t' : topological_space α} :
theorem continuous_id_of_le {α : Type u} {t t' : topological_space α} (h : t t') :
theorem mem_nhds_induced {α : Type u} {β : Type v} [T : topological_space α] (f : β → α) (a : β) (s : set β) :
s nhds a ∃ (u : set α) (H : u nhds (f a)), f ⁻¹' u s
theorem nhds_induced {α : Type u} {β : Type v} [T : topological_space α] (f : β → α) (a : β) :
nhds a = filter.comap f (nhds (f a))
theorem induced_iff_nhds_eq {α : Type u} {β : Type v} [tα : topological_space α] [tβ : topological_space β] (f : β → α) :
= topological_space.induced f ∀ (b : β), nhds b = filter.comap f (nhds (f b))
theorem map_nhds_induced_of_surjective {α : Type u} {β : Type v} [T : topological_space α] {f : β → α} (hf : function.surjective f) (a : β) :
filter.map f (nhds a) = nhds (f a)
theorem is_open_induced_eq {α : Type u_1} {β : Type u_2} [t : topological_space β] {f : α → β} {s : set α} :
is_open s s set.preimage f '' {s : set β | is_open s}
theorem is_open_induced {α : Type u_1} {β : Type u_2} [t : topological_space β] {f : α → β} {s : set β} (h : is_open s) :
theorem map_nhds_induced_eq {α : Type u_1} {β : Type u_2} [t : topological_space β] {f : α → β} (a : α) :
theorem map_nhds_induced_of_mem {α : Type u_1} {β : Type u_2} [t : topological_space β] {f : α → β} {a : α} (h : set.range f nhds (f a)) :
filter.map f (nhds a) = nhds (f a)
theorem closure_induced {α : Type u_1} {β : Type u_2} [t : topological_space β] {f : α → β} {a : α} {s : set α} :
a closure s f a closure (f '' s)
theorem is_closed_induced_iff' {α : Type u_1} {β : Type u_2} [t : topological_space β] {f : α → β} {s : set α} :
is_closed s ∀ (a : α), f a closure (f '' s)a s
@[simp]
@[simp]
@[simp]
theorem nhds_false  :
theorem continuous_Prop {α : Type u_1} [topological_space α] {p : α → Prop} :
continuous p is_open {x : α | p x}
theorem is_open_iff_continuous_mem {α : Type u_1} [topological_space α] {s : set α} :
is_open s continuous (λ (x : α), x s)
theorem set_of_is_open_sup {α : Type u} (t₁ t₂ : topological_space α) :
{s : set α | (t₁ t₂).is_open s} = {s : set α | t₁.is_open s} {s : set α | t₂.is_open s}
theorem generate_from_Union {α : Type u} {ι : Sort v} {f : ι → set (set α)} :
topological_space.generate_from (⋃ (i : ι), f i) = ⨅ (i : ι), topological_space.generate_from (f i)
theorem set_of_is_open_supr {α : Type u} {ι : Sort v} {t : ι → topological_space α} :
{s : set α | (⨆ (i : ι), t i).is_open s} = ⋂ (i : ι), {s : set α | (t i).is_open s}
theorem generate_from_sUnion {α : Type u} {S : set (set (set α))} :
theorem set_of_is_open_Sup {α : Type u} {T : set (topological_space α)} :
{s : set α | (has_Sup.Sup T).is_open s} = ⋂ (t : topological_space α) (H : t T), {s : set α | t.is_open s}
theorem generate_from_union_is_open {α : Type u} (a b : topological_space α) :
topological_space.generate_from ({s : set α | a.is_open s} {s : set α | b.is_open s}) = a b
theorem generate_from_Union_is_open {α : Type u} {ι : Sort v} (f : ι → topological_space α) :
topological_space.generate_from (⋃ (i : ι), {s : set α | (f i).is_open s}) = ⨅ (i : ι), f i
theorem generate_from_inter {α : Type u} (a b : topological_space α) :
topological_space.generate_from ({s : set α | a.is_open s} {s : set α | b.is_open s}) = a b
theorem generate_from_Inter {α : Type u} {ι : Sort v} (f : ι → topological_space α) :
topological_space.generate_from (⋂ (i : ι), {s : set α | (f i).is_open s}) = ⨆ (i : ι), f i
theorem generate_from_Inter_of_generate_from_eq_self {α : Type u} {ι : Sort v} (f : ι → set (set α)) (hf : ∀ (i : ι), {s : set α | (topological_space.generate_from (f i)).is_open s} = f i) :
topological_space.generate_from (⋂ (i : ι), f i) = ⨆ (i : ι), topological_space.generate_from (f i)
theorem is_open_supr_iff {α : Type u} {ι : Sort v} {t : ι → topological_space α} {s : set α} :
is_open s ∀ (i : ι), is_open s
theorem is_closed_supr_iff {α : Type u} {ι : Sort v} {t : ι → topological_space α} {s : set α} :
is_closed s ∀ (i : ι), is_closed s