Theorems · Theorem · general topology
lt_mem_nhds
∀ {α : Type u} [ts : TopologicalSpace α] [inst : Preorder α] [OrderTopology α] {a b : α},
a < b → ∀ᶠ (x : α) in nhds b, a < x- Defined in
- Mathlib.Topology.Order.Basic
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 60 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
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
- Filter.Eventuallystatement · cited by 3,134
- OrderTopologystatement and proof · cited by 1,355
- IsOpen.mem_nhdsproof · cited by 470
- isOpen_lt'proof · cited by 8
Cited by20
Results whose statement or proof uses this declaration.
- Filter.Tendsto.atTop_mul_posproof · cited by 7
- Real.hasStrictFDerivAt_rpow_of_posproof · cited by 4
- MeasureTheory.hasSum_integral_measureproof · cited by 4
- Real.contDiffAt_rpow_of_neproof · cited by 4
- IsLUB.exists_seq_strictMono_tendsto_of_notMemproof · cited by 4
- Filter.Tendsto.add_atTopproof · cited by 3
- EReal.continuousAt_add_top_coeproof · cited by 2
- Filter.Tendsto.mul_atTop'proof · cited by 2
- Real.deriv_arcsin_auxproof · cited by 2
- expNegInvGlue.hasDerivAt_polynomial_eval_inv_mulproof · cited by 2
- ENNReal.tendsto_subproof · cited by 2
- le_mem_nhdsproof · cited by 2