Theorems · Theorem · general topology
mem_nhds_iff_exists_Ioo_subset
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [NoMaxOrder α] [NoMinOrder α]
{a : α} {s : Set α}, s ∈ nhds a ↔ ∃ l u, a ∈ Set.Ioo l u ∧ Set.Ioo l u ⊆ sA set is a neighborhood of a if and only if it contains an interval (l, u) containing a.
- Defined in
- Mathlib.Topology.Order.Basic
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound
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.
- Setstatement and proof · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- LinearOrderstatement and proof · cited by 8,572
- Filterstatement · cited by 8,121
- nhdsstatement · cited by 5,554
- OrderTopologystatement and proof · cited by 1,355
- Set.Ioostatement · cited by 1,214
- NoMaxOrderstatement and proof · cited by 340
- NoMinOrderstatement and proof · cited by 247
- NoMaxOrder.exists_gtproof · cited by 62
- NoMinOrder.exists_ltproof · cited by 41
- mem_nhds_iff_exists_Ioo_subset'proof · cited by 3
Cited by13
Results whose statement or proof uses this declaration.
- ProbabilityTheory.aemeasurable_of_mem_interior_integrableExpSetproof · cited by 6
- ProbabilityTheory.hasDerivAt_integral_pow_mul_expproof · cited by 3
- ConvexOn.hasDerivWithinAt_sInf_slope_of_mem_interiorproof · cited by 2
- ConvexOn.hasDerivWithinAt_sSup_slope_of_mem_interiorproof · cited by 2
- Real.isTopologicalBasis_Ioo_ratproof · cited by 2
- ConvexOn.leftDeriv_le_rightDeriv_of_mem_interiorproof · cited by 2
- intervalIntegral.sub_le_integral_of_hasDeriv_right_of_le_Icoproof · cited by 1
- Filter.Eventually.exists_Ioo_subsetproof · cited by 1
- ConvexOn.monotoneOn_leftDerivproof · cited by 0