Theorems · Theorem · general topology

tendsto_atTop_of_monotone

∀ {ι : Type u_3} {α : Type u_4} [inst : Preorder ι] [inst_1 : TopologicalSpace α]
  [inst_2 : ConditionallyCompleteLinearOrder α] [OrderTopology α] {f : ι → α},
  Monotone f → Filter.Tendsto f Filter.atTop Filter.atTop ∨ ∃ l, Filter.Tendsto f Filter.atTop (nhds l)

Defined in: Mathlib.Topology.Order.MonotoneConvergence
Cited by: 7 results in Mathlib
Foundations: Depth 68 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Preorder TopologicalSpace ConditionallyCompleteLinearOrder OrderTopology

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites13

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

TopologicalSpacestatement and proof · cited by 24,529
Preorderstatement and proof · cited by 7,952
nhdsstatement · cited by 5,554
Set.rangeproof · cited by 4,705
Filter.Tendstostatement · cited by 3,814
iSupproof · cited by 2,415
Filter.atTopstatement · cited by 2,405
Monotonestatement and proof · cited by 1,397
OrderTopologystatement and proof · cited by 1,355
BddAboveproof · cited by 620
ConditionallyCompleteLinearOrderstatement and proof · cited by 542
tendsto_atTop_ciSupproof · cited by 13

Cited by7

Results whose statement or proof uses this declaration.

tendsto_atTop_of_antitoneproof · cited by 4
NNReal.not_summable_iff_tendsto_nat_atTopproof · cited by 2
tendsto_iff_tendsto_subseq_of_monotoneproof · cited by 2
tendsto_atBot_of_monotoneproof · cited by 1
MeasureTheory.tendsto_of_lintegral_tendsto_of_monotone_auxproof · cited by 1
tendsto_of_monotoneproof · cited by 0
StieltjesFunction.isFiniteMeasure_of_forall_abs_leproof · cited by 0