# 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

- `TopologicalSpace.induced f : TopologicalSpace β → TopologicalSpace α`;
- `TopologicalSpace.coinduced f : TopologicalSpace α → TopologicalSpace β`.

Continuity, the ordering on topologies and (co)induced topologies are related as follows:

- The identity map `(α, t₁) → (α, t₂)` is continuous iff `t₁ ≤ t₂`.
- A map `f : (α, t) → (β, u)` is continuous
  - iff `t ≤ TopologicalSpace.induced f u` (`continuous_iff_le_induced`)
  - iff `TopologicalSpace.coinduced f t ≤ u` (`continuous_iff_coinduced_le`).

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

For a function `f : α → β`, `(TopologicalSpace.coinduced f, TopologicalSpace.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. More precisely, we use the corresponding Galois coinsertion between topologies on `α` (with the reversed inclusion ordering) and collections of sets in `α` (with the reversed inclusion ordering).

## Tags #

finer, coarser, induced topology, coinduced topology

source
inductive TopologicalSpace.GenerateOpen {α : Type u} (g : Set (Set α)) :
Set α → Prop

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

- basic {α : Type u} {g : Set (Set α)} (s : Set α) : s ∈ g → GenerateOpen g s
- univ {α : Type u} {g : Set (Set α)} : GenerateOpen g Set.univ
- inter {α : Type u} {g : Set (Set α)} (s t : Set α) : GenerateOpen g s → GenerateOpen g t → GenerateOpen g (s ∩ t)
- sUnion {α : Type u} {g : Set (Set α)} (S : Set (Set α)) : (∀ s ∈ S, GenerateOpen g s) → GenerateOpen g (⋃₀ S)

Instances For

source
def TopologicalSpace.generateFrom {α : Type u} (g : Set (Set α)) :
TopologicalSpace α

The smallest topological space containing the collection `g` of basic sets

Equations

- TopologicalSpace.generateFrom g = { IsOpen := TopologicalSpace.GenerateOpen g, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }

Instances For

source
theorem TopologicalSpace.isOpen_generateFrom_of_mem {α : Type u} {g : Set (Set α)} {s : Set α} (hs : s ∈ g) :
IsOpen s
source
theorem TopologicalSpace.nhds_generateFrom {α : Type u} {g : Set (Set α)} {a : α} :
nhds a = ⨅ s ∈ {s : Set α | a ∈ s ∧ s ∈ g}, Filter.principal s
source
theorem TopologicalSpace.tendsto_nhds_generateFrom_iff {α : Type u} {β : Type u_1} {m : α → β} {f : Filter α} {g : Set (Set β)} {b : β} :
Filter.Tendsto m f (nhds b) ↔ ∀ s ∈ g, b ∈ s → m ⁻¹' s ∈ f
source
def TopologicalSpace.mkOfNhds {α : Type u} (n : α → Filter α) :
TopologicalSpace α

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

Equations

- TopologicalSpace.mkOfNhds n = { IsOpen := fun (s : Set α) => ∀ a ∈ s, s ∈ n a, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }

Instances For

source
theorem TopologicalSpace.nhds_mkOfNhds_of_hasBasis {α : Type u} {n : α → Filter α} {ι : α → Sort u_1} {p : (a : α) → ι a → Prop} {s : (a : α) → ι a → Set α} (hb : ∀ (a : α), (n a).HasBasis (p a) (s a)) (hpure : ∀ (a : α) (i : ι a), p a i → a ∈ s a i) (hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x) (a : α) :
nhds a = n a
source
theorem TopologicalSpace.nhds_mkOfNhds {α : Type u} (n : α → Filter α) (a : α) (h₀ : pure ≤ n) (h₁ : ∀ (a : α), ∀ s ∈ n a, ∀ᶠ (y : α) in n a, s ∈ n y) :
nhds a = n a
source
theorem TopologicalSpace.nhds_mkOfNhds_single {α : Type u} [DecidableEq α] {a₀ : α} {l : Filter α} (h : pure a₀ ≤ l) (b : α) :
nhds b = Function.update pure a₀ l b
source
theorem TopologicalSpace.nhds_mkOfNhds_filterBasis {α : Type u} (B : α → FilterBasis α) (a : α) (h₀ : ∀ (x : α), ∀ n ∈ B x, x ∈ n) (h₁ : ∀ (x : α), ∀ n ∈ B x, ∃ n₁ ∈ B x, ∀ x' ∈ n₁, ∃ n₂ ∈ B x', n₂ ⊆ n) :
nhds a = (B a).filter
source
instance TopologicalSpace.instPartialOrder {α : Type u} :
PartialOrder (TopologicalSpace α)

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

- One or more equations did not get rendered due to their size.

source
theorem TopologicalSpace.le_def {α : Type u_1} {t s : TopologicalSpace α} :
t ≤ s ↔ IsOpen ≤ IsOpen
source
theorem TopologicalSpace.le_generateFrom_iff_subset_isOpen {α : Type u} {g : Set (Set α)} {t : TopologicalSpace α} :
t ≤ generateFrom g ↔ g ⊆ {s : Set α | IsOpen s}
source
def TopologicalSpace.mkOfClosure {α : Type u} (s : Set (Set α)) (hs : {u : Set α | GenerateOpen s u} = s) :
TopologicalSpace α

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

Equations

- TopologicalSpace.mkOfClosure s hs = { IsOpen := fun (u : Set α) => u ∈ s, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }

Instances For

source
theorem TopologicalSpace.mkOfClosure_sets {α : Type u} {s : Set (Set α)} {hs : {u : Set α | GenerateOpen s u} = s} :
TopologicalSpace.mkOfClosure s hs = generateFrom s
source
theorem TopologicalSpace.gc_generateFrom (α : Type u_1) :
GaloisConnection (fun (t : TopologicalSpace α) => OrderDual.toDual {s : Set α | IsOpen s}) (generateFrom ∘ ⇑OrderDual.ofDual)
source
def TopologicalSpace.gciGenerateFrom (α : Type u_1) :
GaloisCoinsertion (fun (t : TopologicalSpace α) => OrderDual.toDual {s : Set α | IsOpen s}) (generateFrom ∘ ⇑OrderDual.ofDual)

The Galois coinsertion between `TopologicalSpace α` and `(Set (Set α))ᵒᵈ` whose lower part sends a topology to its collection of open subsets, and whose upper part sends a collection of subsets of `α` to the topology they generate.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
instance TopologicalSpace.instCompleteLattice {α : Type u} :
CompleteLattice (TopologicalSpace α)

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

- TopologicalSpace.instCompleteLattice = (TopologicalSpace.gciGenerateFrom α).liftCompleteLattice

source
theorem TopologicalSpace.generateFrom_anti {α : Type u_1} {g₁ g₂ : Set (Set α)} (h : g₁ ⊆ g₂) :
generateFrom g₂ ≤ generateFrom g₁
source
theorem TopologicalSpace.generateFrom_setOf_isOpen {α : Type u} (t : TopologicalSpace α) :
generateFrom {s : Set α | IsOpen s} = t
source
theorem TopologicalSpace.leftInverse_generateFrom {α : Type u} :
Function.LeftInverse generateFrom fun (t : TopologicalSpace α) => {s : Set α | IsOpen s}
source
theorem TopologicalSpace.generateFrom_surjective {α : Type u} :
Function.Surjective generateFrom
source
theorem TopologicalSpace.setOf_isOpen_injective {α : Type u} :
Function.Injective fun (t : TopologicalSpace α) => {s : Set α | IsOpen s}
source
theorem IsOpen.mono {α : Type u_1} {t₁ t₂ : TopologicalSpace α} {s : Set α} (hs : IsOpen s) (h : t₁ ≤ t₂) :
IsOpen s
source
theorem IsClosed.mono {α : Type u_1} {t₁ t₂ : TopologicalSpace α} {s : Set α} (hs : IsClosed s) (h : t₁ ≤ t₂) :
IsClosed s
source
theorem closure.mono {α : Type u_1} {t₁ t₂ : TopologicalSpace α} {s : Set α} (h : t₁ ≤ t₂) :
closure s ⊆ closure s
source
theorem isOpen_implies_isOpen_iff {α : Type u_1} {t₁ t₂ : TopologicalSpace α} :
(∀ (s : Set α), IsOpen s → IsOpen s) ↔ t₂ ≤ t₁
source
theorem TopologicalSpace.isOpen_top_iff {α : Type u_2} (U : Set α) :
IsOpen U ↔ U = ∅ ∨ U = Set.univ

The only open sets in the indiscrete topology are the empty set and the whole space.

source
class DiscreteTopology (α : Type u_2) [t : TopologicalSpace α] :
Prop

A topological space is discrete if every set is open, that is, its topology equals the discrete topology `⊥`.

- eq_bot : t = ⊥

  The `TopologicalSpace` structure on a type with discrete topology is equal to `⊥`.

Instances

source
theorem discreteTopology_bot (α : Type u_2) :
DiscreteTopology α
source
@[simp]
theorem isOpen_discrete {α : Type u_1} [TopologicalSpace α] [DiscreteTopology α] (s : Set α) :
IsOpen s
source
@[simp]
theorem isClosed_discrete {α : Type u_1} [TopologicalSpace α] [DiscreteTopology α] (s : Set α) :
IsClosed s
source
theorem closure_discrete {α : Type u_1} [TopologicalSpace α] [DiscreteTopology α] (s : Set α) :
closure s = s
source
@[simp]
theorem dense_discrete {α : Type u_1} [TopologicalSpace α] [DiscreteTopology α] {s : Set α} :
Dense s ↔ s = Set.univ
source
@[simp]
theorem denseRange_discrete {α : Type u_1} [TopologicalSpace α] [DiscreteTopology α] {ι : Type u_3} {f : ι → α} :
DenseRange f ↔ Function.Surjective f
source
theorem continuous_of_discreteTopology {α : Type u_1} [TopologicalSpace α] [DiscreteTopology α] {β : Type u_2} [TopologicalSpace β] {f : α → β} :
Continuous f
source
theorem continuous_discrete_rng {β : Type u_2} {α : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [DiscreteTopology β] {f : α → β} :
Continuous f ↔ ∀ (b : β), IsOpen (f ⁻¹' {b})

A function to a discrete topological space is continuous if and only if the preimage of every singleton is open.

source
@[simp]
theorem nhds_discrete (α : Type u_3) [TopologicalSpace α] [DiscreteTopology α] :
nhds = pure
source
theorem mem_nhds_discrete {α : Type u_1} [TopologicalSpace α] [DiscreteTopology α] {x : α} {s : Set α} :
s ∈ nhds x ↔ x ∈ s
source
theorem le_of_nhds_le_nhds {α : Type u_1} {t₁ t₂ : TopologicalSpace α} (h : ∀ (x : α), nhds x ≤ nhds x) :
t₁ ≤ t₂
source
theorem eq_bot_of_singletons_open {α : Type u_1} {t : TopologicalSpace α} (h : ∀ (x : α), IsOpen {x}) :
t = ⊥
source
theorem discreteTopology_iff_forall_isOpen {α : Type u_1} [TopologicalSpace α] :
DiscreteTopology α ↔ ∀ (s : Set α), IsOpen s
source
@[deprecated discreteTopology_iff_forall_isOpen (since := "2025-10-10")]
theorem forall_open_iff_discrete {X : Type u_2} [TopologicalSpace X] :
(∀ (s : Set X), IsOpen s) ↔ DiscreteTopology X
source
theorem discreteTopology_iff_forall_isClosed {α : Type u_1} [TopologicalSpace α] :
DiscreteTopology α ↔ ∀ (s : Set α), IsClosed s
source
theorem discreteTopology_iff_isOpen_singleton {α : Type u_1} [TopologicalSpace α] :
DiscreteTopology α ↔ ∀ (a : α), IsOpen {a}
source
@[deprecated discreteTopology_iff_isOpen_singleton (since := "2025-10-10")]
theorem singletons_open_iff_discrete {X : Type u_2} [TopologicalSpace X] :
(∀ (a : X), IsOpen {a}) ↔ DiscreteTopology X
source
theorem DiscreteTopology.of_finite_of_isClosed_singleton {α : Type u_1} [TopologicalSpace α] [Finite α] (h : ∀ (a : α), IsClosed {a}) :
DiscreteTopology α
source
theorem discreteTopology_iff_singleton_mem_nhds {α : Type u_1} [TopologicalSpace α] :
DiscreteTopology α ↔ ∀ (x : α), {x} ∈ nhds x
source
theorem discreteTopology_iff_nhds {α : Type u_1} [TopologicalSpace α] :
DiscreteTopology α ↔ ∀ (x : α), nhds x = pure x

This lemma characterizes discrete topological spaces as those whose singletons are neighbourhoods.

source
theorem discreteTopology_iff_nhds_ne {α : Type u_1} [TopologicalSpace α] :
DiscreteTopology α ↔ ∀ (x : α), nhdsWithin x {x}ᶜ = ⊥
source
theorem DiscreteTopology.of_continuous_injective {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] [DiscreteTopology β] {f : α → β} (hc : Continuous f) (hinj : Function.Injective f) :
DiscreteTopology α

If the codomain of a continuous injective function has discrete topology, then so does the domain.

See also `Embedding.discreteTopology` for an important special case.

source
theorem isOpen_induced_iff {α : Type u_1} {β : Type u_2} [t : TopologicalSpace β] {s : Set α} {f : α → β} :
IsOpen s ↔ ∃ (t_1 : Set β), IsOpen t_1 ∧ f ⁻¹' t_1 = s
source
theorem isClosed_induced_iff {α : Type u_1} {β : Type u_2} [t : TopologicalSpace β] {s : Set α} {f : α → β} :
IsClosed s ↔ ∃ (t_1 : Set β), IsClosed t_1 ∧ f ⁻¹' t_1 = s
source
theorem isOpen_coinduced {α : Type u_1} {β : Type u_2} {t : TopologicalSpace α} {s : Set β} {f : α → β} :
IsOpen s ↔ IsOpen (f ⁻¹' s)
source
theorem isClosed_coinduced {α : Type u_1} {β : Type u_2} {t : TopologicalSpace α} {s : Set β} {f : α → β} :
IsClosed s ↔ IsClosed (f ⁻¹' s)
source
theorem preimage_nhds_coinduced {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {π : α → β} {s : Set β} {a : α} (hs : s ∈ nhds (π a)) :
π ⁻¹' s ∈ nhds a
source
theorem Continuous.coinduced_le {α : Type u_1} {β : Type u_2} {t : TopologicalSpace α} {t' : TopologicalSpace β} {f : α → β} (h : Continuous f) :
TopologicalSpace.coinduced f t ≤ t'
source
theorem coinduced_le_iff_le_induced {α : Type u_1} {β : Type u_2} {f : α → β} {tα : TopologicalSpace α} {tβ : TopologicalSpace β} :
TopologicalSpace.coinduced f tα ≤ tβ ↔ tα ≤ TopologicalSpace.induced f tβ
source
theorem Continuous.le_induced {α : Type u_1} {β : Type u_2} {t : TopologicalSpace α} {t' : TopologicalSpace β} {f : α → β} (h : Continuous f) :
t ≤ TopologicalSpace.induced f t'
source
theorem gc_coinduced_induced {α : Type u_1} {β : Type u_2} (f : α → β) :
GaloisConnection (TopologicalSpace.coinduced f) (TopologicalSpace.induced f)
source
theorem induced_mono {α : Type u_1} {β : Type u_2} {t₁ t₂ : TopologicalSpace α} {g : β → α} (h : t₁ ≤ t₂) :
TopologicalSpace.induced g t₁ ≤ TopologicalSpace.induced g t₂
source
theorem coinduced_mono {α : Type u_1} {β : Type u_2} {t₁ t₂ : TopologicalSpace α} {f : α → β} (h : t₁ ≤ t₂) :
TopologicalSpace.coinduced f t₁ ≤ TopologicalSpace.coinduced f t₂
source
@[simp]
theorem induced_top {α : Type u_1} {β : Type u_2} {g : β → α} :
TopologicalSpace.induced g ⊤ = ⊤
source
@[simp]
theorem induced_inf {α : Type u_1} {β : Type u_2} {t₁ t₂ : TopologicalSpace α} {g : β → α} :
TopologicalSpace.induced g (t₁ ⊓ t₂) = TopologicalSpace.induced g t₁ ⊓ TopologicalSpace.induced g t₂
source
@[simp]
theorem induced_iInf {α : Type u_1} {β : Type u_2} {g : β → α} {ι : Sort w} {t : ι → TopologicalSpace α} :
TopologicalSpace.induced g (⨅ (i : ι), t i) = ⨅ (i : ι), TopologicalSpace.induced g (t i)
source
@[simp]
theorem induced_sInf {α : Type u_1} {β : Type u_2} {g : β → α} {s : Set (TopologicalSpace α)} :
TopologicalSpace.induced g (sInf s) = sInf (TopologicalSpace.induced g '' s)
source
@[simp]
theorem coinduced_bot {α : Type u_1} {β : Type u_2} {f : α → β} :
TopologicalSpace.coinduced f ⊥ = ⊥
source
@[simp]
theorem coinduced_sup {α : Type u_1} {β : Type u_2} {t₁ t₂ : TopologicalSpace α} {f : α → β} :
TopologicalSpace.coinduced f (t₁ ⊔ t₂) = TopologicalSpace.coinduced f t₁ ⊔ TopologicalSpace.coinduced f t₂
source
@[simp]
theorem coinduced_iSup {α : Type u_1} {β : Type u_2} {f : α → β} {ι : Sort w} {t : ι → TopologicalSpace α} :
TopologicalSpace.coinduced f (⨆ (i : ι), t i) = ⨆ (i : ι), TopologicalSpace.coinduced f (t i)
source
@[simp]
theorem coinduced_sSup {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set (TopologicalSpace α)} :
TopologicalSpace.coinduced f (sSup s) = sSup (TopologicalSpace.coinduced f '' s)
source
theorem induced_id {α : Type u_1} [t : TopologicalSpace α] :
TopologicalSpace.induced id t = t
source
theorem induced_compose {α : Type u_1} {β : Type u_2} {γ : Type u_3} {tγ : TopologicalSpace γ} {f : α → β} {g : β → γ} :
TopologicalSpace.induced f (TopologicalSpace.induced g tγ) = TopologicalSpace.induced (g ∘ f) tγ
source
theorem induced_const {α : Type u_1} {β : Type u_2} [t : TopologicalSpace α] {x : α} :
TopologicalSpace.induced (fun (x_1 : β) => x) t = ⊤
source
theorem coinduced_id {α : Type u_1} [t : TopologicalSpace α] :
TopologicalSpace.coinduced id t = t
source
theorem coinduced_compose {α : Type u_1} {β : Type u_2} {γ : Type u_3} [tα : TopologicalSpace α] {f : α → β} {g : β → γ} :
TopologicalSpace.coinduced g (TopologicalSpace.coinduced f tα) = TopologicalSpace.coinduced (g ∘ f) tα
source
theorem Equiv.induced_symm {α : Type u_4} {β : Type u_5} (e : α ≃ β) :
TopologicalSpace.induced ⇑e.symm = TopologicalSpace.coinduced ⇑e
source
theorem Equiv.coinduced_symm {α : Type u_4} {β : Type u_5} (e : α ≃ β) :
TopologicalSpace.coinduced ⇑e.symm = TopologicalSpace.induced ⇑e
source
instance inhabitedTopologicalSpace {α : Type u} :
Inhabited (TopologicalSpace α)
Equations

- inhabitedTopologicalSpace = { default := ⊥ }

source
@[instance 100]
instance Subsingleton.uniqueTopologicalSpace {α : Type u} [Subsingleton α] :
Unique (TopologicalSpace α)
Equations

- Subsingleton.uniqueTopologicalSpace = { default := ⊥, uniq := ⋯ }

source
@[instance 100]
instance Subsingleton.discreteTopology {α : Type u} [t : TopologicalSpace α] [Subsingleton α] :
DiscreteTopology α
source
instance instTopologicalSpaceEmpty :
TopologicalSpace Empty
Equations

- instTopologicalSpaceEmpty = ⊥

source
instance instDiscreteTopologyEmpty :
DiscreteTopology Empty
source
instance instTopologicalSpacePEmpty :
TopologicalSpace PEmpty.{u_1 + 1}
Equations

- instTopologicalSpacePEmpty = ⊥

source
instance instDiscreteTopologyPEmpty :
DiscreteTopology PEmpty.{u_1 + 1}
source
instance instTopologicalSpacePUnit :
TopologicalSpace PUnit.{u_1 + 1}
Equations

- instTopologicalSpacePUnit = ⊥

source
instance instDiscreteTopologyPUnit :
DiscreteTopology PUnit.{u_1 + 1}
source
instance instTopologicalSpaceBool :
TopologicalSpace Bool
Equations

- instTopologicalSpaceBool = ⊥

source
instance instDiscreteTopologyBool :
DiscreteTopology Bool
source
instance instTopologicalSpaceNat :
TopologicalSpace ℕ
Equations

- instTopologicalSpaceNat = ⊥

source
instance instDiscreteTopologyNat :
DiscreteTopology ℕ
source
instance instTopologicalSpaceInt :
TopologicalSpace ℤ
Equations

- instTopologicalSpaceInt = ⊥

source
instance instDiscreteTopologyInt :
DiscreteTopology ℤ
source
instance instTopologicalSpaceFin {n : ℕ} :
TopologicalSpace (Fin n)
Equations

- instTopologicalSpaceFin = ⊥

source
instance instDiscreteTopologyFin {n : ℕ} :
DiscreteTopology (Fin n)
source
theorem Nat.cast_continuous {R : Type u_1} [NatCast R] [TopologicalSpace R] :
Continuous Nat.cast
source
theorem Int.cast_continuous {R : Type u_1} [IntCast R] [TopologicalSpace R] :
Continuous Int.cast
source
instance sierpinskiSpace :
TopologicalSpace Prop
Equations

- sierpinskiSpace = TopologicalSpace.generateFrom {{True}}

source
theorem continuous_empty_function {α : Type u} {β : Type v} [TopologicalSpace α] [TopologicalSpace β] [IsEmpty β] (f : α → β) :
Continuous f

See also `continuous_of_discreteTopology`, which works for `IsEmpty α`.

source
theorem le_generateFrom {α : Type u} {t : TopologicalSpace α} {g : Set (Set α)} (h : ∀ s ∈ g, IsOpen s) :
t ≤ TopologicalSpace.generateFrom g
source
theorem induced_generateFrom_eq {α : Type u_1} {β : Type u_2} {b : Set (Set β)} {f : α → β} :
TopologicalSpace.induced f (TopologicalSpace.generateFrom b) = TopologicalSpace.generateFrom (Set.preimage f '' b)
source
theorem le_induced_generateFrom {α : Type u_1} {β : Type u_2} [t : TopologicalSpace α] {b : Set (Set β)} {f : α → β} (h : ∀ a ∈ b, IsOpen (f ⁻¹' a)) :
t ≤ TopologicalSpace.induced f (TopologicalSpace.generateFrom b)
source
theorem generateFrom_insert_of_generateOpen {α : Type u_1} {s : Set (Set α)} {t : Set α} (ht : TopologicalSpace.GenerateOpen s t) :
TopologicalSpace.generateFrom (insert t s) = TopologicalSpace.generateFrom s
source
@[simp]
theorem generateFrom_insert_univ {α : Type u_1} {s : Set (Set α)} :
TopologicalSpace.generateFrom (insert Set.univ s) = TopologicalSpace.generateFrom s
source
@[simp]
theorem generateFrom_insert_empty {α : Type u_1} {s : Set (Set α)} :
TopologicalSpace.generateFrom (insert ∅ s) = TopologicalSpace.generateFrom s
source
def nhdsAdjoint {α : Type u} (a : α) (f : Filter α) :
TopologicalSpace α

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

Equations

- nhdsAdjoint a f = { IsOpen := fun (s : Set α) => a ∈ s → s ∈ f, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }

Instances For

source
theorem gc_nhds {α : Type u} (a : α) :
GaloisConnection (nhdsAdjoint a) fun (t : TopologicalSpace α) => nhds a
source
theorem nhds_mono {α : Type u} {t₁ t₂ : TopologicalSpace α} {a : α} (h : t₁ ≤ t₂) :
nhds a ≤ nhds a
source
theorem le_iff_nhds {α : Type u_1} (t t' : TopologicalSpace α) :
t ≤ t' ↔ ∀ (x : α), nhds x ≤ nhds x
source
theorem isOpen_singleton_nhdsAdjoint {α : Type u_1} {a b : α} (f : Filter α) (hb : b ≠ a) :
IsOpen {b}
source
theorem nhds_nhdsAdjoint_same {α : Type u} (a : α) (f : Filter α) :
nhds a = pure a ⊔ f
source
theorem nhds_nhdsAdjoint_of_ne {α : Type u} {a b : α} (f : Filter α) (h : b ≠ a) :
nhds b = pure b
source
theorem nhds_nhdsAdjoint {α : Type u} [DecidableEq α] (a : α) (f : Filter α) :
nhds = Function.update pure a (pure a ⊔ f)
source
theorem le_nhdsAdjoint_iff' {α : Type u} {a : α} {f : Filter α} {t : TopologicalSpace α} :
t ≤ nhdsAdjoint a f ↔ nhds a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → nhds b = pure b
source
theorem le_nhdsAdjoint_iff {α : Type u_1} (a : α) (f : Filter α) (t : TopologicalSpace α) :
t ≤ nhdsAdjoint a f ↔ nhds a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → IsOpen {b}
source
theorem nhds_iInf {α : Type u} {ι : Sort u_1} {t : ι → TopologicalSpace α} {a : α} :
nhds a = ⨅ (i : ι), nhds a
source
theorem nhds_sInf {α : Type u} {s : Set (TopologicalSpace α)} {a : α} :
nhds a = ⨅ t ∈ s, nhds a
source
theorem nhds_inf {α : Type u} {t₁ t₂ : TopologicalSpace α} {a : α} :
nhds a = nhds a ⊓ nhds a
source
theorem nhds_top {α : Type u} {a : α} :
nhds a = ⊤
source
theorem isOpen_sup {α : Type u} {t₁ t₂ : TopologicalSpace α} {s : Set α} :
IsOpen s ↔ IsOpen s ∧ IsOpen s
source
@[simp]
theorem inseparable_top {α : Type u} (x y : α) :
Inseparable x y

In the trivial topology no points are separable.

The corresponding `bot` lemma is handled more generally by `inseparable_iff_eq`.

source
theorem TopologicalSpace.eq_top_iff_forall_inseparable {α : Type u} {t : TopologicalSpace α} :
t = ⊤ ↔ ∀ (x y : α), Inseparable x y
source
theorem TopologicalSpace.ne_top_iff_exists_not_inseparable {α : Type u} {t : TopologicalSpace α} :
t ≠ ⊤ ↔ ∃ (x : α) (y : α), ¬Inseparable x y
source
theorem continuous_iff_coinduced_le {α : Type u} {β : Type v} {f : α → β} {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace β} :
Continuous f ↔ TopologicalSpace.coinduced f t₁ ≤ t₂
source
theorem continuous_iff_le_induced {α : Type u} {β : Type v} {f : α → β} {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace β} :
Continuous f ↔ t₁ ≤ TopologicalSpace.induced f t₂
source
theorem continuous_generateFrom_iff {α : Type u} {β : Type v} {f : α → β} {t : TopologicalSpace α} {b : Set (Set β)} :
Continuous f ↔ ∀ s ∈ b, IsOpen (f ⁻¹' s)
source
theorem continuous_induced_dom {α : Type u} {β : Type v} {f : α → β} {t : TopologicalSpace β} :
Continuous f
source
theorem continuous_induced_rng {α : Type u} {β : Type v} {γ : Type u_1} {f : α → β} {g : γ → α} {t₂ : TopologicalSpace β} {t₁ : TopologicalSpace γ} :
Continuous g ↔ Continuous (f ∘ g)
source
theorem continuous_coinduced_rng {α : Type u} {β : Type v} {f : α → β} {t : TopologicalSpace α} :
Continuous f
source
theorem continuous_coinduced_dom {α : Type u} {β : Type v} {γ : Type u_1} {f : α → β} {g : β → γ} {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace γ} :
Continuous g ↔ Continuous (g ∘ f)
source
theorem continuous_le_dom {α : Type u} {β : Type v} {f : α → β} {t₁ t₂ : TopologicalSpace α} {t₃ : TopologicalSpace β} (h₁ : t₂ ≤ t₁) (h₂ : Continuous f) :
Continuous f
source
theorem continuous_le_rng {α : Type u} {β : Type v} {f : α → β} {t₁ : TopologicalSpace α} {t₂ t₃ : TopologicalSpace β} (h₁ : t₂ ≤ t₃) (h₂ : Continuous f) :
Continuous f
source
theorem continuous_sup_dom {α : Type u} {β : Type v} {f : α → β} {t₁ t₂ : TopologicalSpace α} {t₃ : TopologicalSpace β} :
Continuous f ↔ Continuous f ∧ Continuous f
source
theorem continuous_sup_rng_left {α : Type u} {β : Type v} {f : α → β} {t₁ : TopologicalSpace α} {t₃ t₂ : TopologicalSpace β} :
Continuous f → Continuous f
source
theorem continuous_sup_rng_right {α : Type u} {β : Type v} {f : α → β} {t₁ : TopologicalSpace α} {t₃ t₂ : TopologicalSpace β} :
Continuous f → Continuous f
source
theorem continuous_sSup_dom {α : Type u} {β : Type v} {f : α → β} {T : Set (TopologicalSpace α)} {t₂ : TopologicalSpace β} :
Continuous f ↔ ∀ t ∈ T, Continuous f
source
theorem continuous_sSup_rng {α : Type u} {β : Type v} {f : α → β} {t₁ : TopologicalSpace α} {t₂ : Set (TopologicalSpace β)} {t : TopologicalSpace β} (h₁ : t ∈ t₂) (hf : Continuous f) :
Continuous f
source
theorem continuous_iSup_dom {α : Type u} {β : Type v} {f : α → β} {ι : Sort u_2} {t₁ : ι → TopologicalSpace α} {t₂ : TopologicalSpace β} :
Continuous f ↔ ∀ (i : ι), Continuous f
source
theorem continuous_iSup_rng {α : Type u} {β : Type v} {f : α → β} {ι : Sort u_2} {t₁ : TopologicalSpace α} {t₂ : ι → TopologicalSpace β} {i : ι} (h : Continuous f) :
Continuous f
source
theorem continuous_inf_rng {α : Type u} {β : Type v} {f : α → β} {t₁ : TopologicalSpace α} {t₂ t₃ : TopologicalSpace β} :
Continuous f ↔ Continuous f ∧ Continuous f
source
theorem continuous_inf_dom_left {α : Type u} {β : Type v} {f : α → β} {t₁ t₂ : TopologicalSpace α} {t₃ : TopologicalSpace β} :
Continuous f → Continuous f
source
theorem continuous_inf_dom_right {α : Type u} {β : Type v} {f : α → β} {t₁ t₂ : TopologicalSpace α} {t₃ : TopologicalSpace β} :
Continuous f → Continuous f
source
theorem continuous_sInf_dom {α : Type u} {β : Type v} {f : α → β} {t₁ : Set (TopologicalSpace α)} {t₂ : TopologicalSpace β} {t : TopologicalSpace α} (h₁ : t ∈ t₁) :
Continuous f → Continuous f
source
theorem continuous_sInf_rng {α : Type u} {β : Type v} {f : α → β} {t₁ : TopologicalSpace α} {T : Set (TopologicalSpace β)} :
Continuous f ↔ ∀ t ∈ T, Continuous f
source
theorem continuous_iInf_dom {α : Type u} {β : Type v} {f : α → β} {ι : Sort u_2} {t₁ : ι → TopologicalSpace α} {t₂ : TopologicalSpace β} {i : ι} :
Continuous f → Continuous f
source
theorem continuous_iInf_rng {α : Type u} {β : Type v} {f : α → β} {ι : Sort u_2} {t₁ : TopologicalSpace α} {t₂ : ι → TopologicalSpace β} :
Continuous f ↔ ∀ (i : ι), Continuous f
source
theorem continuous_bot {α : Type u} {β : Type v} {f : α → β} {t : TopologicalSpace β} :
Continuous f
source
theorem continuous_top {α : Type u} {β : Type v} {f : α → β} {t : TopologicalSpace α} :
Continuous f
source
theorem continuous_id_iff_le {α : Type u} {t t' : TopologicalSpace α} :
Continuous id ↔ t ≤ t'
source
theorem continuous_id_of_le {α : Type u} {t t' : TopologicalSpace α} (h : t ≤ t') :
Continuous id
source
theorem mem_nhds_induced {α : Type u} {β : Type v} [T : TopologicalSpace α] (f : β → α) (a : β) (s : Set β) :
s ∈ nhds a ↔ ∃ u ∈ nhds (f a), f ⁻¹' u ⊆ s
source
theorem nhds_induced {α : Type u} {β : Type v} [T : TopologicalSpace α] (f : β → α) (a : β) :
nhds a = Filter.comap f (nhds (f a))
source
theorem induced_iff_nhds_eq {α : Type u} {β : Type v} [tα : TopologicalSpace α] [tβ : TopologicalSpace β] (f : β → α) :
tβ = TopologicalSpace.induced f tα ↔ ∀ (b : β), nhds b = Filter.comap f (nhds (f b))
source
theorem map_nhds_induced_of_surjective {α : Type u} {β : Type v} [T : TopologicalSpace α] {f : β → α} (hf : Function.Surjective f) (a : β) :
Filter.map f (nhds a) = nhds (f a)
source
theorem continuous_nhdsAdjoint_dom {α : Type u} {β : Type v} [TopologicalSpace β] {f : α → β} {a : α} {l : Filter α} :
Continuous f ↔ Filter.Tendsto f l (nhds (f a))
source
theorem coinduced_nhdsAdjoint {α : Type u} {β : Type v} (f : α → β) (a : α) (l : Filter α) :
TopologicalSpace.coinduced f (nhdsAdjoint a l) = nhdsAdjoint (f a) (Filter.map f l)
source
theorem isOpen_induced_eq {α : Type u_1} {β : Type u_2} [t : TopologicalSpace β] {f : α → β} {s : Set α} :
IsOpen s ↔ s ∈ Set.preimage f '' {s : Set β | IsOpen s}
source
theorem isOpen_induced {α : Type u_1} {β : Type u_2} [t : TopologicalSpace β] {f : α → β} {s : Set β} (h : IsOpen s) :
IsOpen (f ⁻¹' s)
source
theorem map_nhds_induced_eq {α : Type u_1} {β : Type u_2} [t : TopologicalSpace β] {f : α → β} (a : α) :
Filter.map f (nhds a) = nhdsWithin (f a) (Set.range f)
source
theorem map_nhds_induced_of_mem {α : Type u_1} {β : Type u_2} [t : TopologicalSpace β] {f : α → β} {a : α} (h : Set.range f ∈ nhds (f a)) :
Filter.map f (nhds a) = nhds (f a)
source
theorem closure_induced {α : Type u_1} {β : Type u_2} [t : TopologicalSpace β] {f : α → β} {a : α} {s : Set α} :
a ∈ closure s ↔ f a ∈ closure (f '' s)
source
theorem isClosed_induced_iff' {α : Type u_1} {β : Type u_2} [t : TopologicalSpace β] {f : α → β} {s : Set α} :
IsClosed s ↔ ∀ (a : α), f a ∈ closure (f '' s) → a ∈ s
source
@[simp]
theorem isOpen_singleton_true :
IsOpen {True}
source
@[simp]
theorem nhds_true :
nhds True = pure True
source
@[simp]
theorem nhds_false :
nhds False = ⊤
source
theorem tendsto_nhds_true {α : Type u_1} {l : Filter α} {p : α → Prop} :
Filter.Tendsto p l (nhds True) ↔ ∀ᶠ (x : α) in l, p x
source
theorem tendsto_nhds_Prop {α : Type u_1} {l : Filter α} {p : α → Prop} {q : Prop} :
Filter.Tendsto p l (nhds q) ↔ q → ∀ᶠ (x : α) in l, p x
source
theorem continuous_Prop {α : Type u_1} [TopologicalSpace α] {p : α → Prop} :
Continuous p ↔ IsOpen {x : α | p x}
source
theorem isOpen_iff_continuous_mem {α : Type u_1} [TopologicalSpace α] {s : Set α} :
IsOpen s ↔ Continuous fun (x : α) => x ∈ s
source
theorem generateFrom_union {α : Type u} (a₁ a₂ : Set (Set α)) :
TopologicalSpace.generateFrom (a₁ ∪ a₂) = TopologicalSpace.generateFrom a₁ ⊓ TopologicalSpace.generateFrom a₂
source
theorem setOf_isOpen_sup {α : Type u} (t₁ t₂ : TopologicalSpace α) :
{s : Set α | IsOpen s} = {s : Set α | IsOpen s} ∩ {s : Set α | IsOpen s}
source
theorem generateFrom_iUnion {α : Type u} {ι : Sort v} {f : ι → Set (Set α)} :
TopologicalSpace.generateFrom (⋃ (i : ι), f i) = ⨅ (i : ι), TopologicalSpace.generateFrom (f i)
source
theorem setOf_isOpen_iSup {α : Type u} {ι : Sort v} {t : ι → TopologicalSpace α} :
{s : Set α | IsOpen s} = ⋂ (i : ι), {s : Set α | IsOpen s}
source
theorem generateFrom_sUnion {α : Type u} {S : Set (Set (Set α))} :
TopologicalSpace.generateFrom (⋃₀ S) = ⨅ s ∈ S, TopologicalSpace.generateFrom s
source
theorem setOf_isOpen_sSup {α : Type u} {T : Set (TopologicalSpace α)} :
{s : Set α | IsOpen s} = ⋂ t ∈ T, {s : Set α | IsOpen s}
source
theorem generateFrom_union_isOpen {α : Type u} (a b : TopologicalSpace α) :
TopologicalSpace.generateFrom ({s : Set α | IsOpen s} ∪ {s : Set α | IsOpen s}) = a ⊓ b
source
theorem generateFrom_iUnion_isOpen {α : Type u} {ι : Sort v} (f : ι → TopologicalSpace α) :
TopologicalSpace.generateFrom (⋃ (i : ι), {s : Set α | IsOpen s}) = ⨅ (i : ι), f i
source
theorem generateFrom_inter {α : Type u} (a b : TopologicalSpace α) :
TopologicalSpace.generateFrom ({s : Set α | IsOpen s} ∩ {s : Set α | IsOpen s}) = a ⊔ b
source
theorem generateFrom_iInter {α : Type u} {ι : Sort v} (f : ι → TopologicalSpace α) :
TopologicalSpace.generateFrom (⋂ (i : ι), {s : Set α | IsOpen s}) = ⨆ (i : ι), f i
source
theorem generateFrom_iInter_of_generateFrom_eq_self {α : Type u} {ι : Sort v} (f : ι → Set (Set α)) (hf : ∀ (i : ι), {s : Set α | IsOpen s} = f i) :
TopologicalSpace.generateFrom (⋂ (i : ι), f i) = ⨆ (i : ι), TopologicalSpace.generateFrom (f i)
source
theorem isOpen_iSup_iff {α : Type u} {ι : Sort v} {t : ι → TopologicalSpace α} {s : Set α} :
IsOpen s ↔ ∀ (i : ι), IsOpen s
source
theorem isOpen_sSup_iff {α : Type u} {s : Set α} {T : Set (TopologicalSpace α)} :
IsOpen s ↔ ∀ t ∈ T, IsOpen s
source
theorem isClosed_iSup_iff {α : Type u} {ι : Sort v} {t : ι → TopologicalSpace α} {s : Set α} :
IsClosed s ↔ ∀ (i : ι), IsClosed s
source
theorem isClosed_sSup_iff {α : Type u} {s : Set α} {T : Set (TopologicalSpace α)} :
IsClosed s ↔ ∀ t ∈ T, IsClosed s