Order topology on WithTop ι

When ι is a topological space with the order topology, we also endow WithTop ι with the order topology. If ι is second countable, we prove that WithTop ι also is.

instance TopologicalSpace.instWithTopOfOrderTopology {ι : Type u_1} [Preorder ι] [TopologicalSpace ι] [OrderTopology ι] : TopologicalSpace (WithTop ι)

Equations

• TopologicalSpace.instWithTopOfOrderTopology = Preorder.topology (WithTop ι)

instance TopologicalSpace.instOrderTopologyWithTop {ι : Type u_1} [Preorder ι] [TopologicalSpace ι] [OrderTopology ι] : OrderTopology (WithTop ι)

instance TopologicalSpace.instSecondCountableTopologyWithTop {ι : Type u_1} [Preorder ι] [ts : TopologicalSpace ι] [ht : OrderTopology ι] [SecondCountableTopology ι] : SecondCountableTopology (WithTop ι)

theorem WithTop.isEmbedding_coe {ι : Type u_1} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] : Topology.IsEmbedding some

theorem WithTop.isOpenEmbedding_coe {ι : Type u_1} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] : Topology.IsOpenEmbedding some

theorem WithTop.nhds_coe {ι : Type u_1} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] {r : ι} : nhds ↑r = Filter.map some (nhds r)

theorem WithTop.continuous_coe {ι : Type u_1} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] : Continuous some

theorem WithTop.tendsto_untopD {ι : Type u_1} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] (d : ι) {a : WithTop ι} (ha : a ≠ ⊤) : Filter.Tendsto (untopD d) (nhds a) (nhds (untopD d a))

theorem WithTop.continuousOn_untopD {ι : Type u_1} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] (d : ι) : ContinuousOn (untopD d) {a : WithTop ι | a ≠ ⊤}

theorem WithTop.tendsto_untopA {ι : Type u_1} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [Nonempty ι] {a : WithTop ι} (ha : a ≠ ⊤) : Filter.Tendsto untopA (nhds a) (nhds a.untopA)

theorem WithTop.continuousOn_untopA {ι : Type u_1} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [Nonempty ι] : ContinuousOn untopA {a : WithTop ι | a ≠ ⊤}

theorem WithTop.tendsto_untop {ι : Type u_1} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] (a : ↑{a : WithTop ι | a ≠ ⊤}) : Filter.Tendsto (fun (x : ↑{a : WithTop ι | a ≠ ⊤}) => (↑x).untop ⋯) (nhds a) (nhds ((↑a).untop ⋯))

theorem WithTop.continuous_untop {ι : Type u_1} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] : Continuous fun (x : ↑{a : WithTop ι | a ≠ ⊤}) => (↑x).untop ⋯

noncomputable def WithTop.neTopHomeomorph (ι : Type u_1) [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] : ↑{a : WithTop ι | a ≠ ⊤} ≃ₜ ι

Homeomorphism between the non-top elements of WithTop ι and ι.

Equations

• WithTop.neTopHomeomorph ι = { toEquiv := Equiv.withTopSubtypeNe, continuous_toFun := ⋯, continuous_invFun := ⋯ }

noncomputable def WithTop.sumHomeomorph (ι : Type u_1) [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [OrderTop ι] : WithTop ι ≃ₜ ι ⊕ Unit

If ι has a top element, then WithTop ι is homeomorphic to ι ⊕ Unit.

Equations

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