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.

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance TopologicalSpace.instWithBotOfOrderTopology {ι : Type u_1} [Preorder ι] [TopologicalSpace ι] [OrderTopology ι] : TopologicalSpace (WithBot ι)

Equations

• TopologicalSpace.instWithBotOfOrderTopology = Preorder.topology (WithBot ι)

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

instance TopologicalSpace.instOrderTopologyWithBot {ι : Type u_1} [Preorder ι] [TopologicalSpace ι] [OrderTopology ι] : OrderTopology (WithBot ι)

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 WithBot.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 WithBot.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 WithBot.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 WithBot.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 WithBot.tendsto_unbotD {ι : Type u_1} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] (d : ι) {a : WithBot ι} (ha : a ≠ ⊥) : Filter.Tendsto (unbotD d) (nhds a) (nhds (unbotD d a))

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

theorem WithBot.continuousOn_unbotD {ι : Type u_1} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] (d : ι) : ContinuousOn (unbotD d) {a : WithBot ι | 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 WithBot.tendsto_unbotA {ι : Type u_1} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [Nonempty ι] {a : WithBot ι} (ha : a ≠ ⊥) : Filter.Tendsto unbotA (nhds a) (nhds a.unbotA)

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

theorem WithBot.continuousOn_unbotA {ι : Type u_1} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [Nonempty ι] : ContinuousOn unbotA {a : WithBot ι | 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 WithBot.tendsto_unbot {ι : Type u_1} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] (a : ↑{a : WithBot ι | a ≠ ⊥}) : Filter.Tendsto (fun (x : ↑{a : WithBot ι | a ≠ ⊥}) => (↑x).unbot ⋯) (nhds a) (nhds ((↑a).unbot ⋯))

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

theorem WithBot.continuous_unbot {ι : Type u_1} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] : Continuous fun (x : ↑{a : WithBot ι | a ≠ ⊥}) => (↑x).unbot ⋯

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 WithBot.neBotHomeomorph (ι : Type u_1) [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] : ↑{a : WithBot ι | a ≠ ⊥} ≃ₜ ι

Homeomorphism between the non-bot elements of WithBot ι and ι.

Equations

• WithBot.neBotHomeomorph ι = { toEquiv := Equiv.withBotSubtypeNe, 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.

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

If ι has a bot element, then WithBot ι is homeomorphic to ι ⊕ Unit.

Equations

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

theorem WithTop.tendsto_nhds_top_iff {ι : Type u_1} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] {α : Type u_2} {f : Filter α} (x : α → WithTop ι) : Filter.Tendsto x f (nhds ⊤) ↔ ∀ (i : ι), ∀ᶠ (a : α) in f, ↑i < x a

theorem WithBot.tendsto_nhds_bot_iff {ι : Type u_1} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] {α : Type u_2} {f : Filter α} (x : α → WithBot ι) : Filter.Tendsto x f (nhds ⊥) ↔ ∀ (i : ι), ∀ᶠ (a : α) in f, x a < ↑i

theorem WithTop.tendsto_coe_atTop {ι : Type u_1} [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [NoMaxOrder ι] : Filter.Tendsto some Filter.atTop (nhds ⊤)