Theorems · Theorem · general topology

Filter.tendsto_atTop_of_monotone_of_filter

∀ {ι : Type u_1} {α : Type u_3} [inst : Preorder ι] [inst_1 : Preorder α] {l : Filter ι} {u : ι → α},
  Monotone u → ∀ [l.NeBot], Filter.Tendsto u l Filter.atTop → Filter.Tendsto u Filter.atTop Filter.atTop

If a monotone function u : ι → α tends to atTop along some non-trivial filter l, then it tends to atTop along atTop.

Defined in

Mathlib.Order.Filter.AtTopBot.Tendsto

Cited by

1 results in Mathlib

Foundations

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

Assumes

PreorderPreorderFilter.NeBot