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

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 ∈ g, TopologicalSpace.GenerateOpen g s
• univ: ∀ {α : Type u} {g : Set (Set α)}, TopologicalSpace.GenerateOpen g Set.univ
• inter: ∀ {α : Type u} {g : Set (Set α)} (s t : Set α), TopologicalSpace.GenerateOpen g s → TopologicalSpace.GenerateOpen g t → TopologicalSpace.GenerateOpen g (s ∩ t)
• sUnion: ∀ {α : Type u} {g : Set (Set α)} (S : Set (Set α)), (∀ s ∈ S, TopologicalSpace.GenerateOpen g s) → TopologicalSpace.GenerateOpen g (⋃₀ S)

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 := ⋯ }

theorem TopologicalSpace.isOpen_generateFrom_of_mem {α : Type u} {g : Set (Set α)} {s : Set α} (hs : s ∈ g) : IsOpen s

theorem TopologicalSpace.nhds_generateFrom {α : Type u} {g : Set (Set α)} {a : α} : nhds a = ⨅ s ∈ {s : Set α | a ∈ s ∧ s ∈ g}, Filter.principal s

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

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 := ⋯ }

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

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

theorem TopologicalSpace.nhds_mkOfNhds_single {α : Type u} [DecidableEq α] {a₀ : α} {l : Filter α} (h : pure a₀ ≤ l) (b : α) : nhds b = Function.update pure a₀ l b

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

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

• TopologicalSpace.instPartialOrder = PartialOrder.mk ⋯

theorem TopologicalSpace.le_def {α : Type u_1} {t s : TopologicalSpace α} : t ≤ s ↔ IsOpen ≤ IsOpen

theorem TopologicalSpace.le_generateFrom_iff_subset_isOpen {α : Type u} {g : Set (Set α)} {t : TopologicalSpace α} : t ≤ TopologicalSpace.generateFrom g ↔ g ⊆ {s : Set α | IsOpen s}

def TopologicalSpace.mkOfClosure {α : Type u} (s : Set (Set α)) (hs : {u : Set α | TopologicalSpace.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 := ⋯ }

theorem TopologicalSpace.mkOfClosure_sets {α : Type u} {s : Set (Set α)} {hs : {u : Set α | TopologicalSpace.GenerateOpen s u} = s} : TopologicalSpace.mkOfClosure s hs = TopologicalSpace.generateFrom s

theorem TopologicalSpace.gc_generateFrom (α : Type u_1) : GaloisConnection (fun (t : TopologicalSpace α) => OrderDual.toDual {s : Set α | IsOpen s}) (TopologicalSpace.generateFrom ∘ ⇑OrderDual.ofDual)

def TopologicalSpace.gciGenerateFrom (α : Type u_1) : GaloisCoinsertion (fun (t : TopologicalSpace α) => OrderDual.toDual {s : Set α | IsOpen s}) (TopologicalSpace.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.

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

theorem TopologicalSpace.generateFrom_anti {α : Type u_1} {g₁ g₂ : Set (Set α)} (h : g₁ ⊆ g₂) : TopologicalSpace.generateFrom g₂ ≤ TopologicalSpace.generateFrom g₁

theorem TopologicalSpace.generateFrom_setOf_isOpen {α : Type u} (t : TopologicalSpace α) : TopologicalSpace.generateFrom {s : Set α | IsOpen s} = t

theorem TopologicalSpace.leftInverse_generateFrom {α : Type u} : Function.LeftInverse TopologicalSpace.generateFrom fun (t : TopologicalSpace α) => {s : Set α | IsOpen s}

theorem TopologicalSpace.generateFrom_surjective {α : Type u} : Function.Surjective TopologicalSpace.generateFrom

theorem TopologicalSpace.setOf_isOpen_injective {α : Type u} : Function.Injective fun (t : TopologicalSpace α) => {s : Set α | IsOpen s}

theorem IsOpen.mono {α : Type u_1} {t₁ t₂ : TopologicalSpace α} {s : Set α} (hs : IsOpen s) (h : t₁ ≤ t₂) : IsOpen s

theorem IsClosed.mono {α : Type u_1} {t₁ t₂ : TopologicalSpace α} {s : Set α} (hs : IsClosed s) (h : t₁ ≤ t₂) : IsClosed s

theorem closure.mono {α : Type u_1} {t₁ t₂ : TopologicalSpace α} {s : Set α} (h : t₁ ≤ t₂) : closure s ⊆ closure s

theorem isOpen_implies_isOpen_iff {α : Type u_1} {t₁ t₂ : TopologicalSpace α} : (∀ (s : Set α), IsOpen s → IsOpen s) ↔ t₂ ≤ t₁

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.

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 ⊥.

theorem discreteTopology_bot (α : Type u_2) : DiscreteTopology α

@[simp]

theorem isOpen_discrete {α : Type u_1} [TopologicalSpace α] [DiscreteTopology α] (s : Set α) : IsOpen s

@[simp]

theorem isClosed_discrete {α : Type u_1} [TopologicalSpace α] [DiscreteTopology α] (s : Set α) : IsClosed s

@[simp]

theorem closure_discrete {α : Type u_1} [TopologicalSpace α] [DiscreteTopology α] (s : Set α) : closure s = s

@[simp]

theorem dense_discrete {α : Type u_1} [TopologicalSpace α] [DiscreteTopology α] {s : Set α} : Dense s ↔ s = Set.univ

@[simp]

theorem denseRange_discrete {α : Type u_1} [TopologicalSpace α] [DiscreteTopology α] {ι : Type u_3} {f : ι → α} : DenseRange f ↔ Function.Surjective f

theorem continuous_of_discreteTopology {α : Type u_1} [TopologicalSpace α] [DiscreteTopology α] {β : Type u_2} [TopologicalSpace β] {f : α → β} : Continuous f

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.

@[simp]

theorem nhds_discrete (α : Type u_3) [TopologicalSpace α] [DiscreteTopology α] : nhds = pure

theorem mem_nhds_discrete {α : Type u_1} [TopologicalSpace α] [DiscreteTopology α] {x : α} {s : Set α} : s ∈ nhds x ↔ x ∈ s

theorem le_of_nhds_le_nhds {α : Type u_1} {t₁ t₂ : TopologicalSpace α} (h : ∀ (x : α), nhds x ≤ nhds x) : t₁ ≤ t₂

@[deprecated TopologicalSpace.ext_nhds]

theorem eq_of_nhds_eq_nhds {X : Type u_3} {t t' : TopologicalSpace X} : (∀ (x : X), nhds x = nhds x) → t = t'

Alias of the reverse direction of TopologicalSpace.ext_iff_nhds.

---

Alias of the reverse direction of TopologicalSpace.ext_iff_nhds.

theorem eq_bot_of_singletons_open {α : Type u_1} {t : TopologicalSpace α} (h : ∀ (x : α), IsOpen {x}) : t = ⊥

theorem forall_open_iff_discrete {X : Type u_2} [TopologicalSpace X] : (∀ (s : Set X), IsOpen s) ↔ DiscreteTopology X

theorem discreteTopology_iff_forall_isClosed {α : Type u_1} [TopologicalSpace α] : DiscreteTopology α ↔ ∀ (s : Set α), IsClosed s

theorem singletons_open_iff_discrete {X : Type u_2} [TopologicalSpace X] : (∀ (a : X), IsOpen {a}) ↔ DiscreteTopology X

theorem DiscreteTopology.of_finite_of_isClosed_singleton {α : Type u_1} [TopologicalSpace α] [Finite α] (h : ∀ (a : α), IsClosed {a}) : DiscreteTopology α

theorem discreteTopology_iff_singleton_mem_nhds {α : Type u_1} [TopologicalSpace α] : DiscreteTopology α ↔ ∀ (x : α), {x} ∈ nhds x

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.

theorem discreteTopology_iff_nhds_ne {α : Type u_1} [TopologicalSpace α] : DiscreteTopology α ↔ ∀ (x : α), nhdsWithin x {x}ᶜ = ⊥

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.

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

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

theorem isOpen_coinduced {α : Type u_1} {β : Type u_2} {t : TopologicalSpace α} {s : Set β} {f : α → β} : IsOpen s ↔ IsOpen (f ⁻¹' s)

theorem isClosed_coinduced {α : Type u_1} {β : Type u_2} {t : TopologicalSpace α} {s : Set β} {f : α → β} : IsClosed s ↔ IsClosed (f ⁻¹' s)

theorem preimage_nhds_coinduced {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {π : α → β} {s : Set β} {a : α} (hs : s ∈ nhds (π a)) : π ⁻¹' s ∈ nhds a

theorem Continuous.coinduced_le {α : Type u_1} {β : Type u_2} {t : TopologicalSpace α} {t' : TopologicalSpace β} {f : α → β} (h : Continuous f) : TopologicalSpace.coinduced f t ≤ t'

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β

theorem Continuous.le_induced {α : Type u_1} {β : Type u_2} {t : TopologicalSpace α} {t' : TopologicalSpace β} {f : α → β} (h : Continuous f) : t ≤ TopologicalSpace.induced f t'

theorem gc_coinduced_induced {α : Type u_1} {β : Type u_2} (f : α → β) : GaloisConnection (TopologicalSpace.coinduced f) (TopologicalSpace.induced f)

theorem induced_mono {α : Type u_1} {β : Type u_2} {t₁ t₂ : TopologicalSpace α} {g : β → α} (h : t₁ ≤ t₂) : TopologicalSpace.induced g t₁ ≤ TopologicalSpace.induced g t₂

theorem coinduced_mono {α : Type u_1} {β : Type u_2} {t₁ t₂ : TopologicalSpace α} {f : α → β} (h : t₁ ≤ t₂) : TopologicalSpace.coinduced f t₁ ≤ TopologicalSpace.coinduced f t₂

@[simp]

theorem induced_top {α : Type u_1} {β : Type u_2} {g : β → α} : TopologicalSpace.induced g ⊤ = ⊤

@[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₂

@[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)

@[simp]

theorem induced_sInf {α : Type u_1} {β : Type u_2} {g : β → α} {s : Set (TopologicalSpace α)} : TopologicalSpace.induced g (sInf s) = sInf (TopologicalSpace.induced g '' s)

@[simp]

theorem coinduced_bot {α : Type u_1} {β : Type u_2} {f : α → β} : TopologicalSpace.coinduced f ⊥ = ⊥

@[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₂

@[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)

@[simp]

theorem coinduced_sSup {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set (TopologicalSpace α)} : TopologicalSpace.coinduced f (sSup s) = sSup (TopologicalSpace.coinduced f '' s)

theorem induced_id {α : Type u_1} [t : TopologicalSpace α] : TopologicalSpace.induced id t = t

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γ

theorem induced_const {α : Type u_1} {β : Type u_2} [t : TopologicalSpace α] {x : α} : TopologicalSpace.induced (fun (x_1 : β) => x) t = ⊤

theorem coinduced_id {α : Type u_1} [t : TopologicalSpace α] : TopologicalSpace.coinduced id t = t

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α

theorem Equiv.induced_symm {α : Type u_4} {β : Type u_5} (e : α ≃ β) : TopologicalSpace.induced ⇑e.symm = TopologicalSpace.coinduced ⇑e

theorem Equiv.coinduced_symm {α : Type u_4} {β : Type u_5} (e : α ≃ β) : TopologicalSpace.coinduced ⇑e.symm = TopologicalSpace.induced ⇑e

instance inhabitedTopologicalSpace {α : Type u} : Inhabited (TopologicalSpace α)

Equations

• inhabitedTopologicalSpace = { default := ⊥ }

@[instance 100]

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

Equations

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

@[instance 100]

instance Subsingleton.discreteTopology {α : Type u} [t : TopologicalSpace α] [Subsingleton α] : DiscreteTopology α

Equations

• ⋯ = ⋯

instance instTopologicalSpaceEmpty : TopologicalSpace Empty

Equations

• instTopologicalSpaceEmpty = ⊥

instance instDiscreteTopologyEmpty : DiscreteTopology Empty

Equations

• instDiscreteTopologyEmpty = ⋯

instance instTopologicalSpacePEmpty : TopologicalSpace PEmpty.{u_1 + 1}

Equations

• instTopologicalSpacePEmpty = ⊥

instance instDiscreteTopologyPEmpty : DiscreteTopology PEmpty.{u_1 + 1}

Equations

• instDiscreteTopologyPEmpty = ⋯

instance instTopologicalSpacePUnit : TopologicalSpace PUnit.{u_1 + 1}

Equations

• instTopologicalSpacePUnit = ⊥

instance instDiscreteTopologyPUnit : DiscreteTopology PUnit.{u_1 + 1}

Equations

• instDiscreteTopologyPUnit = ⋯

instance instTopologicalSpaceBool : TopologicalSpace Bool

Equations

• instTopologicalSpaceBool = ⊥

instance instDiscreteTopologyBool : DiscreteTopology Bool

Equations

• instDiscreteTopologyBool = ⋯

instance instTopologicalSpaceNat : TopologicalSpace ℕ

Equations

• instTopologicalSpaceNat = ⊥

instance instDiscreteTopologyNat : DiscreteTopology ℕ

Equations

• instDiscreteTopologyNat = ⋯

instance instTopologicalSpaceInt : TopologicalSpace ℤ

Equations

• instTopologicalSpaceInt = ⊥

instance instDiscreteTopologyInt : DiscreteTopology ℤ

Equations

• instDiscreteTopologyInt = ⋯

instance instTopologicalSpaceFin {n : ℕ} : TopologicalSpace (Fin n)

Equations

• instTopologicalSpaceFin = ⊥

instance instDiscreteTopologyFin {n : ℕ} : DiscreteTopology (Fin n)

Equations

• ⋯ = ⋯

instance sierpinskiSpace : TopologicalSpace Prop

Equations

• sierpinskiSpace = TopologicalSpace.generateFrom {{True}}

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

theorem le_generateFrom {α : Type u} {t : TopologicalSpace α} {g : Set (Set α)} (h : ∀ s ∈ g, IsOpen s) : t ≤ TopologicalSpace.generateFrom g

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)

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)

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

@[simp]

theorem generateFrom_insert_univ {α : Type u_1} {s : Set (Set α)} : TopologicalSpace.generateFrom (insert Set.univ s) = TopologicalSpace.generateFrom s

@[simp]

theorem generateFrom_insert_empty {α : Type u_1} {s : Set (Set α)} : TopologicalSpace.generateFrom (insert ∅ s) = TopologicalSpace.generateFrom s

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 := ⋯ }

theorem gc_nhds {α : Type u} (a : α) : GaloisConnection (nhdsAdjoint a) fun (t : TopologicalSpace α) => nhds a

theorem nhds_mono {α : Type u} {t₁ t₂ : TopologicalSpace α} {a : α} (h : t₁ ≤ t₂) : nhds a ≤ nhds a

theorem le_iff_nhds {α : Type u_1} (t t' : TopologicalSpace α) : t ≤ t' ↔ ∀ (x : α), nhds x ≤ nhds x

theorem isOpen_singleton_nhdsAdjoint {α : Type u_1} {a b : α} (f : Filter α) (hb : b ≠ a) : IsOpen {b}

theorem nhds_nhdsAdjoint_same {α : Type u} (a : α) (f : Filter α) : nhds a = pure a ⊔ f

@[deprecated nhds_nhdsAdjoint_same]

theorem nhdsAdjoint_nhds {α : Type u} (a : α) (f : Filter α) : nhds a = pure a ⊔ f

Alias of nhds_nhdsAdjoint_same.

theorem nhds_nhdsAdjoint_of_ne {α : Type u} {a b : α} (f : Filter α) (h : b ≠ a) : nhds b = pure b

@[deprecated nhds_nhdsAdjoint_of_ne]

theorem nhdsAdjoint_nhds_of_ne {α : Type u} (a : α) (f : Filter α) {b : α} (h : b ≠ a) : nhds b = pure b

theorem nhds_nhdsAdjoint {α : Type u} [DecidableEq α] (a : α) (f : Filter α) : nhds = Function.update pure a (pure a ⊔ f)

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

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}

theorem nhds_iInf {α : Type u} {ι : Sort u_1} {t : ι → TopologicalSpace α} {a : α} : nhds a = ⨅ (i : ι), nhds a

theorem nhds_sInf {α : Type u} {s : Set (TopologicalSpace α)} {a : α} : nhds a = ⨅ t ∈ s, nhds a

theorem nhds_inf {α : Type u} {t₁ t₂ : TopologicalSpace α} {a : α} : nhds a = nhds a ⊓ nhds a

theorem nhds_top {α : Type u} {a : α} : nhds a = ⊤

theorem isOpen_sup {α : Type u} {t₁ t₂ : TopologicalSpace α} {s : Set α} : IsOpen s ↔ IsOpen s ∧ IsOpen s

theorem continuous_iff_coinduced_le {α : Type u} {β : Type v} {f : α → β} {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace β} : Continuous f ↔ TopologicalSpace.coinduced f t₁ ≤ t₂

theorem continuous_iff_le_induced {α : Type u} {β : Type v} {f : α → β} {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace β} : Continuous f ↔ t₁ ≤ TopologicalSpace.induced f t₂

theorem continuous_generateFrom_iff {α : Type u} {β : Type v} {f : α → β} {t : TopologicalSpace α} {b : Set (Set β)} : Continuous f ↔ ∀ s ∈ b, IsOpen (f ⁻¹' s)

theorem continuous_induced_dom {α : Type u} {β : Type v} {f : α → β} {t : TopologicalSpace β} : Continuous f

theorem continuous_induced_rng {α : Type u} {β : Type v} {γ : Type u_1} {f : α → β} {g : γ → α} {t₂ : TopologicalSpace β} {t₁ : TopologicalSpace γ} : Continuous g ↔ Continuous (f ∘ g)

theorem continuous_coinduced_rng {α : Type u} {β : Type v} {f : α → β} {t : TopologicalSpace α} : Continuous f

theorem continuous_coinduced_dom {α : Type u} {β : Type v} {γ : Type u_1} {f : α → β} {g : β → γ} {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace γ} : Continuous g ↔ Continuous (g ∘ f)

theorem continuous_le_dom {α : Type u} {β : Type v} {f : α → β} {t₁ t₂ : TopologicalSpace α} {t₃ : TopologicalSpace β} (h₁ : t₂ ≤ t₁) (h₂ : Continuous f) : Continuous f

theorem continuous_le_rng {α : Type u} {β : Type v} {f : α → β} {t₁ : TopologicalSpace α} {t₂ t₃ : TopologicalSpace β} (h₁ : t₂ ≤ t₃) (h₂ : Continuous f) : Continuous f

theorem continuous_sup_dom {α : Type u} {β : Type v} {f : α → β} {t₁ t₂ : TopologicalSpace α} {t₃ : TopologicalSpace β} : Continuous f ↔ Continuous f ∧ Continuous f

theorem continuous_sup_rng_left {α : Type u} {β : Type v} {f : α → β} {t₁ : TopologicalSpace α} {t₃ t₂ : TopologicalSpace β} : Continuous f → Continuous f

theorem continuous_sup_rng_right {α : Type u} {β : Type v} {f : α → β} {t₁ : TopologicalSpace α} {t₃ t₂ : TopologicalSpace β} : Continuous f → Continuous f

theorem continuous_sSup_dom {α : Type u} {β : Type v} {f : α → β} {T : Set (TopologicalSpace α)} {t₂ : TopologicalSpace β} : Continuous f ↔ ∀ t ∈ T, Continuous f

theorem continuous_sSup_rng {α : Type u} {β : Type v} {f : α → β} {t₁ : TopologicalSpace α} {t₂ : Set (TopologicalSpace β)} {t : TopologicalSpace β} (h₁ : t ∈ t₂) (hf : Continuous f) : Continuous f

theorem continuous_iSup_dom {α : Type u} {β : Type v} {f : α → β} {ι : Sort u_2} {t₁ : ι → TopologicalSpace α} {t₂ : TopologicalSpace β} : Continuous f ↔ ∀ (i : ι), Continuous f

theorem continuous_iSup_rng {α : Type u} {β : Type v} {f : α → β} {ι : Sort u_2} {t₁ : TopologicalSpace α} {t₂ : ι → TopologicalSpace β} {i : ι} (h : Continuous f) : Continuous f

theorem continuous_inf_rng {α : Type u} {β : Type v} {f : α → β} {t₁ : TopologicalSpace α} {t₂ t₃ : TopologicalSpace β} : Continuous f ↔ Continuous f ∧ Continuous f

theorem continuous_inf_dom_left {α : Type u} {β : Type v} {f : α → β} {t₁ t₂ : TopologicalSpace α} {t₃ : TopologicalSpace β} : Continuous f → Continuous f

theorem continuous_inf_dom_right {α : Type u} {β : Type v} {f : α → β} {t₁ t₂ : TopologicalSpace α} {t₃ : TopologicalSpace β} : Continuous f → Continuous f

theorem continuous_sInf_dom {α : Type u} {β : Type v} {f : α → β} {t₁ : Set (TopologicalSpace α)} {t₂ : TopologicalSpace β} {t : TopologicalSpace α} (h₁ : t ∈ t₁) : Continuous f → Continuous f

theorem continuous_sInf_rng {α : Type u} {β : Type v} {f : α → β} {t₁ : TopologicalSpace α} {T : Set (TopologicalSpace β)} : Continuous f ↔ ∀ t ∈ T, Continuous f

theorem continuous_iInf_dom {α : Type u} {β : Type v} {f : α → β} {ι : Sort u_2} {t₁ : ι → TopologicalSpace α} {t₂ : TopologicalSpace β} {i : ι} : Continuous f → Continuous f

theorem continuous_iInf_rng {α : Type u} {β : Type v} {f : α → β} {ι : Sort u_2} {t₁ : TopologicalSpace α} {t₂ : ι → TopologicalSpace β} : Continuous f ↔ ∀ (i : ι), Continuous f

theorem continuous_bot {α : Type u} {β : Type v} {f : α → β} {t : TopologicalSpace β} : Continuous f

theorem continuous_top {α : Type u} {β : Type v} {f : α → β} {t : TopologicalSpace α} : Continuous f

theorem continuous_id_iff_le {α : Type u} {t t' : TopologicalSpace α} : Continuous id ↔ t ≤ t'

theorem continuous_id_of_le {α : Type u} {t t' : TopologicalSpace α} (h : t ≤ t') : Continuous id

theorem mem_nhds_induced {α : Type u} {β : Type v} [T : TopologicalSpace α] (f : β → α) (a : β) (s : Set β) : s ∈ nhds a ↔ ∃ u ∈ nhds (f a), f ⁻¹' u ⊆ s

theorem nhds_induced {α : Type u} {β : Type v} [T : TopologicalSpace α] (f : β → α) (a : β) : nhds a = Filter.comap f (nhds (f a))

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))

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)

theorem continuous_nhdsAdjoint_dom {α : Type u} {β : Type v} [TopologicalSpace β] {f : α → β} {a : α} {l : Filter α} : Continuous f ↔ Filter.Tendsto f l (nhds (f a))

theorem coinduced_nhdsAdjoint {α : Type u} {β : Type v} (f : α → β) (a : α) (l : Filter α) : TopologicalSpace.coinduced f (nhdsAdjoint a l) = nhdsAdjoint (f a) (Filter.map f l)

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}

theorem isOpen_induced {α : Type u_1} {β : Type u_2} [t : TopologicalSpace β] {f : α → β} {s : Set β} (h : IsOpen s) : IsOpen (f ⁻¹' s)

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)

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)

theorem closure_induced {α : Type u_1} {β : Type u_2} [t : TopologicalSpace β] {f : α → β} {a : α} {s : Set α} : a ∈ closure s ↔ f a ∈ closure (f '' s)

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

@[simp]

theorem isOpen_singleton_true : IsOpen {True}

@[simp]

theorem nhds_true : nhds True = pure True

@[simp]

theorem nhds_false : nhds False = ⊤

theorem tendsto_nhds_true {α : Type u_1} {l : Filter α} {p : α → Prop} : Filter.Tendsto p l (nhds True) ↔ ∀ᶠ (x : α) in l, p x

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

theorem continuous_Prop {α : Type u_1} [TopologicalSpace α] {p : α → Prop} : Continuous p ↔ IsOpen {x : α | p x}

theorem isOpen_iff_continuous_mem {α : Type u_1} [TopologicalSpace α] {s : Set α} : IsOpen s ↔ Continuous fun (x : α) => x ∈ s

theorem generateFrom_union {α : Type u} (a₁ a₂ : Set (Set α)) : TopologicalSpace.generateFrom (a₁ ∪ a₂) = TopologicalSpace.generateFrom a₁ ⊓ TopologicalSpace.generateFrom a₂

theorem setOf_isOpen_sup {α : Type u} (t₁ t₂ : TopologicalSpace α) : {s : Set α | IsOpen s} = {s : Set α | IsOpen s} ∩ {s : Set α | IsOpen s}

theorem generateFrom_iUnion {α : Type u} {ι : Sort v} {f : ι → Set (Set α)} : TopologicalSpace.generateFrom (⋃ (i : ι), f i) = ⨅ (i : ι), TopologicalSpace.generateFrom (f i)

theorem setOf_isOpen_iSup {α : Type u} {ι : Sort v} {t : ι → TopologicalSpace α} : {s : Set α | IsOpen s} = ⋂ (i : ι), {s : Set α | IsOpen s}

theorem generateFrom_sUnion {α : Type u} {S : Set (Set (Set α))} : TopologicalSpace.generateFrom (⋃₀ S) = ⨅ s ∈ S, TopologicalSpace.generateFrom s

theorem setOf_isOpen_sSup {α : Type u} {T : Set (TopologicalSpace α)} : {s : Set α | IsOpen s} = ⋂ t ∈ T, {s : Set α | IsOpen s}

theorem generateFrom_union_isOpen {α : Type u} (a b : TopologicalSpace α) : TopologicalSpace.generateFrom ({s : Set α | IsOpen s} ∪ {s : Set α | IsOpen s}) = a ⊓ b

theorem generateFrom_iUnion_isOpen {α : Type u} {ι : Sort v} (f : ι → TopologicalSpace α) : TopologicalSpace.generateFrom (⋃ (i : ι), {s : Set α | IsOpen s}) = ⨅ (i : ι), f i

theorem generateFrom_inter {α : Type u} (a b : TopologicalSpace α) : TopologicalSpace.generateFrom ({s : Set α | IsOpen s} ∩ {s : Set α | IsOpen s}) = a ⊔ b

theorem generateFrom_iInter {α : Type u} {ι : Sort v} (f : ι → TopologicalSpace α) : TopologicalSpace.generateFrom (⋂ (i : ι), {s : Set α | IsOpen s}) = ⨆ (i : ι), f i

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)

theorem isOpen_iSup_iff {α : Type u} {ι : Sort v} {t : ι → TopologicalSpace α} {s : Set α} : IsOpen s ↔ ∀ (i : ι), IsOpen s

theorem isOpen_sSup_iff {α : Type u} {s : Set α} {T : Set (TopologicalSpace α)} : IsOpen s ↔ ∀ t ∈ T, IsOpen s

theorem isClosed_iSup_iff {α : Type u} {ι : Sort v} {t : ι → TopologicalSpace α} {s : Set α} : IsClosed s ↔ ∀ (i : ι), IsClosed s

theorem isClosed_sSup_iff {α : Type u} {s : Set α} {T : Set (TopologicalSpace α)} : IsClosed s ↔ ∀ t ∈ T, IsClosed s