Theorems · Theorem · real analysis
Filter.Eventually.exists_gt
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : Preorder α] {a : α} [(nhdsWithin a (Set.Ioi a)).NeBot]
{p : α → Prop}, (∀ᶠ (x : α) in nhds a, p x) → ∃ b, a < b ∧ p b- Defined in
- Mathlib.Topology.Order.LeftRight
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
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
- Filter.Eventuallystatement and proof · cited by 3,134
- nhdsWithinstatement and proof · cited by 1,912
- Set.Ioistatement and proof · cited by 1,463
- Filter.NeBotstatement and proof · cited by 853
- Filter.Frequently.and_eventuallyproof · cited by 49
- Filter.Frequently.existsproof · cited by 32
- frequently_gt_nhdsproof · cited by 1
Cited by7
Results whose statement or proof uses this declaration.
- Asymptotics.isLittleOTVS_oneproof · cited by 4
- Metric.exists_forall_closedEBall_subset_aux₁proof · cited by 3
- ConvexOn.continuousOn_tfaeproof · cited by 3
- bddAbove_slope_gt_of_mem_interiorproof · cited by 2
- Convex.interior_closure_eq_interior_of_nonempty_interiorproof · cited by 1
- Asymptotics.Filter.Tendsto.isBigOTVS_oneproof · cited by 1
- Vitali.exists_disjoint_covering_aeproof · cited by 1