Theorems · Theorem · general topology

DenseRange.exists_seq_strictMono_tendsto_of_lt

∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {β : Type u_3}
  [inst_3 : LinearOrder β] [DenselyOrdered α] [FirstCountableTopology α] {f : β → α} {x y : α},
  DenseRange f →
    Monotone f →
      y < x → ∃ u, StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Set.Ioo y x) ∧ Filter.Tendsto (f ∘ u) Filter.atTop (nhds x)

Defined in

Mathlib.Topology.Order.IsLUB

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceLinearOrderOrderTopologyLinearOrderDenselyOrderedFirstCountableTopology