Theorems · Theorem · general topology

tendsto_iff_tendsto_subseq_of_monotone

∀ {ι₁ : Type u_3} {ι₂ : Type u_4} {α : Type u_5} [inst : SemilatticeSup ι₁] [inst_1 : Preorder ι₂] [Nonempty ι₁]
  [inst_3 : TopologicalSpace α] [inst_4 : ConditionallyCompleteLinearOrder α] [OrderTopology α] [NoMaxOrder α]
  {f : ι₂ → α} {φ : ι₁ → ι₂} {l : α},
  Monotone f →
    Filter.Tendsto φ Filter.atTop Filter.atTop →
      (Filter.Tendsto f Filter.atTop (nhds l) ↔ Filter.Tendsto (f ∘ φ) Filter.atTop (nhds l))

Defined in

Mathlib.Topology.Order.MonotoneConvergence

Cited by

2 results in Mathlib

Foundations

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

Assumes

SemilatticeSupPreorderNonemptyTopologicalSpaceConditionallyCompleteLinearOrderOrderTopologyNoMaxOrder