Theorems · Theorem · general topology

WithBot.tendsto_unbot

∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι] (a : ↑{a | a ≠ ⊥}),
  Filter.Tendsto (fun x => (↑x).unbot ⋯) (nhds a) (nhds ((↑a).unbot ⋯))

Defined in

Mathlib.Topology.Order.WithTop

Cited by

1 results in Mathlib

Foundations

Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

LinearOrderTopologicalSpaceOrderTopology