Theorems · Theorem · general topology

isGLB_of_tendsto_atTop

∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder α] [OrderClosedTopology α]
  [inst_3 : Preorder β] [IsDirectedOrder β] [Nonempty β] {f : β → α} {a : α},
  Antitone f → Filter.Tendsto f Filter.atTop (nhds a) → IsGLB (Set.range f) a

Defined in: Mathlib.Topology.Order.MonotoneConvergence
Cited by: 1 results in Mathlib
Foundations: Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: TopologicalSpace Preorder OrderClosedTopology Preorder IsDirectedOrder Nonempty

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites12

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 and proof · cited by 5,554
Set.rangestatement · cited by 4,705
Filter.Tendstostatement and proof · cited by 3,814
Filter.atTopstatement and proof · cited by 2,405
Antitonestatement and proof · cited by 563
OrderClosedTopologystatement and proof · cited by 445
IsDirectedOrderstatement and proof · cited by 316
IsGLBstatement · cited by 213
Antitone.dual_leftproof · cited by 33
isGLB_of_tendsto_atBotproof · cited by 1

Cited by1

Results whose statement or proof uses this declaration.

BoxIntegral.Box.iUnion_Ioo_of_tendstoproof · cited by 0