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 ifft₁ ≤ 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).
- iff
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
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)
Instances For
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
@[deprecated TopologicalSpace.tendsto_nhds_generateFrom_iff]
theorem
TopologicalSpace.tendsto_nhds_generateFrom
{α : Type u}
{β : Type u_1}
{m : α → β}
{f : Filter α}
{g : Set (Set β)}
{b : β}
:
(∀ s ∈ g, b ∈ s → m ⁻¹' s ∈ f) → Filter.Tendsto m f (nhds b)
Alias of the reverse direction of TopologicalSpace.tendsto_nhds_generateFrom_iff.
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
theorem
TopologicalSpace.nhds_mkOfNhds_of_hasBasis
{α : Type u}
{n : α → Filter α}
{ι : α → Sort u_1}
{p : (a : α) → ι a → Prop}
{s : (a : α) → ι a → Set α}
(hb : ∀ (a : α), Filter.HasBasis (n a) (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 : α)
:
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 = FilterBasis.filter (B a)
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.instPartialOrderTopologicalSpace = let __src := PartialOrder.lift (fun (t : TopologicalSpace α) => OrderDual.toDual IsOpen) ⋯; PartialOrder.mk ⋯
theorem
TopologicalSpace.le_generateFrom_iff_subset_isOpen
{α : Type u}
{g : Set (Set α)}
{t : TopologicalSpace α}
:
def
TopologicalSpace.mkOfClosure
{α : Type u}
(s : Set (Set α))
(hs : {u : Set α | TopologicalSpace.GenerateOpen s u} = s)
:
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
theorem
TopologicalSpace.mkOfClosure_sets
{α : Type u}
{s : Set (Set α)}
{hs : {u : Set α | TopologicalSpace.GenerateOpen s u} = 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.
Instances For
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.instCompleteLatticeTopologicalSpace = GaloisCoinsertion.liftCompleteLattice (TopologicalSpace.gciGenerateFrom α)
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₁ : TopologicalSpace α}
{t₂ : TopologicalSpace α}
{s : Set α}
(hs : IsOpen s)
(h : t₁ ≤ t₂)
:
IsOpen s
theorem
IsClosed.mono
{α : Type u_1}
{t₁ : TopologicalSpace α}
{t₂ : TopologicalSpace α}
{s : Set α}
(hs : IsClosed s)
(h : t₁ ≤ t₂)
:
IsClosed s
theorem
closure.mono
{α : Type u_1}
{t₁ : TopologicalSpace α}
{t₂ : TopologicalSpace α}
{s : Set α}
(h : t₁ ≤ t₂)
:
theorem
isOpen_implies_isOpen_iff
{α : Type u_1}
{t₁ : TopologicalSpace α}
{t₂ : TopologicalSpace α}
:
A topological space is discrete if every set is open, that is,
its topology equals the discrete topology ⊥.
The
TopologicalSpacestructure on a type with discrete topology is equal to⊥.
Instances
@[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]
@[simp]
@[simp]
theorem
denseRange_discrete
{α : Type u_1}
[TopologicalSpace α]
[DiscreteTopology α]
{ι : Type u_3}
{f : ι → α}
:
theorem
continuous_of_discreteTopology
{α : Type u_1}
[TopologicalSpace α]
[DiscreteTopology α]
{β : Type u_2}
[TopologicalSpace β]
{f : α → β}
:
theorem
continuous_discrete_rng
{α : Type u_1}
[TopologicalSpace α]
{β : Type u_2}
[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
mem_nhds_discrete
{α : Type u_1}
[TopologicalSpace α]
[DiscreteTopology α]
{x : α}
{s : Set α}
:
theorem
le_of_nhds_le_nhds
{α : Type u_1}
{t₁ : TopologicalSpace α}
{t₂ : TopologicalSpace α}
(h : ∀ (x : α), nhds x ≤ nhds x)
:
t₁ ≤ t₂
@[deprecated TopologicalSpace.ext_nhds]
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})
:
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_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)
:
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_coinduced
{α : Type u_1}
{β : Type u_2}
{t : TopologicalSpace α}
{s : Set β}
{f : α → β}
:
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
induced_mono
{α : Type u_1}
{β : Type u_2}
{t₁ : TopologicalSpace α}
{t₂ : TopologicalSpace α}
{g : β → α}
(h : t₁ ≤ t₂)
:
theorem
coinduced_mono
{α : Type u_1}
{β : Type u_2}
{t₁ : TopologicalSpace α}
{t₂ : TopologicalSpace α}
{f : α → β}
(h : t₁ ≤ t₂)
:
@[simp]
@[simp]
theorem
induced_inf
{α : Type u_1}
{β : Type u_2}
{t₁ : TopologicalSpace α}
{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]
@[simp]
theorem
coinduced_sup
{α : Type u_1}
{β : Type u_2}
{t₁ : TopologicalSpace α}
{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)
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_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
Equations
- ⋯ = ⋯
Equations
Equations
Equations
Equations
- ⋯ = ⋯
Equations
theorem
continuous_empty_function
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[TopologicalSpace β]
[IsEmpty β]
(f : α → β)
:
theorem
le_generateFrom
{α : Type u}
{t : TopologicalSpace α}
{g : Set (Set α)}
(h : ∀ s ∈ g, IsOpen s)
:
theorem
le_induced_generateFrom
{α : Type u_1}
{β : Type u_2}
[t : TopologicalSpace α]
{b : Set (Set β)}
{f : α → β}
(h : ∀ a ∈ b, IsOpen (f ⁻¹' a))
:
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
theorem
gc_nhds
{α : Type u}
(a : α)
:
GaloisConnection (nhdsAdjoint a) fun (t : TopologicalSpace α) => nhds a
theorem
nhds_mono
{α : Type u}
{t₁ : TopologicalSpace α}
{t₂ : TopologicalSpace α}
{a : α}
(h : t₁ ≤ t₂)
:
@[deprecated nhds_nhdsAdjoint_same]
Alias of nhds_nhdsAdjoint_same.
theorem
nhds_nhdsAdjoint
{α : Type u}
[DecidableEq α]
(a : α)
(f : Filter α)
:
nhds = Function.update pure a (pure a ⊔ f)
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)
@[deprecated continuous_generateFrom_iff]
theorem
continuous_generateFrom
{α : Type u}
{β : Type v}
{f : α → β}
{t : TopologicalSpace α}
{b : Set (Set β)}
:
(∀ s ∈ b, IsOpen (f ⁻¹' s)) → Continuous f
Alias of the reverse direction of continuous_generateFrom_iff.
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_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₁ : TopologicalSpace α}
{t₂ : TopologicalSpace α}
{t₃ : TopologicalSpace β}
(h₁ : t₂ ≤ t₁)
(h₂ : Continuous f)
:
theorem
continuous_le_rng
{α : Type u}
{β : Type v}
{f : α → β}
{t₁ : TopologicalSpace α}
{t₂ : TopologicalSpace β}
{t₃ : TopologicalSpace β}
(h₁ : t₂ ≤ t₃)
(h₂ : Continuous f)
:
theorem
continuous_sup_dom
{α : Type u}
{β : Type v}
{f : α → β}
{t₁ : TopologicalSpace α}
{t₂ : TopologicalSpace α}
{t₃ : TopologicalSpace β}
:
Continuous f ↔ Continuous f ∧ Continuous f
theorem
continuous_sup_rng_left
{α : Type u}
{β : Type v}
{f : α → β}
{t₁ : TopologicalSpace α}
{t₃ : TopologicalSpace β}
{t₂ : TopologicalSpace β}
:
Continuous f → Continuous f
theorem
continuous_sup_rng_right
{α : Type u}
{β : Type v}
{f : α → β}
{t₁ : TopologicalSpace α}
{t₃ : TopologicalSpace β}
{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)
:
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)
:
theorem
continuous_inf_rng
{α : Type u}
{β : Type v}
{f : α → β}
{t₁ : TopologicalSpace α}
{t₂ : TopologicalSpace β}
{t₃ : TopologicalSpace β}
:
Continuous f ↔ Continuous f ∧ Continuous f
theorem
continuous_inf_dom_left
{α : Type u}
{β : Type v}
{f : α → β}
{t₁ : TopologicalSpace α}
{t₂ : TopologicalSpace α}
{t₃ : TopologicalSpace β}
:
Continuous f → Continuous f
theorem
continuous_inf_dom_right
{α : Type u}
{β : Type v}
{f : α → β}
{t₁ : TopologicalSpace α}
{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_id_iff_le
{α : Type u}
{t : TopologicalSpace α}
{t' : TopologicalSpace α}
:
Continuous id ↔ t ≤ t'
theorem
continuous_id_of_le
{α : Type u}
{t : TopologicalSpace α}
{t' : TopologicalSpace α}
(h : t ≤ t')
:
Continuous id
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
isOpen_induced_eq
{α : Type u_1}
{β : Type u_2}
[t : TopologicalSpace β]
{f : α → β}
{s : Set α}
:
theorem
isOpen_induced
{α : Type u_1}
{β : Type u_2}
[t : TopologicalSpace β]
{f : α → β}
{s : Set β}
(h : IsOpen 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
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_iUnion
{α : Type u}
{ι : Sort v}
{f : ι → Set (Set α)}
:
TopologicalSpace.generateFrom (⋃ (i : ι), f i) = ⨅ (i : ι), TopologicalSpace.generateFrom (f i)
theorem
generateFrom_sUnion
{α : Type u}
{S : Set (Set (Set α))}
:
TopologicalSpace.generateFrom (⋃₀ S) = ⨅ s ∈ S, TopologicalSpace.generateFrom s
theorem
generateFrom_iUnion_isOpen
{α : Type u}
{ι : Sort v}
(f : ι → TopologicalSpace α)
:
TopologicalSpace.generateFrom (⋃ (i : ι), {s : Set α | IsOpen s}) = ⨅ (i : ι), f i
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)