Theorems · Theorem · general topology
Ioo_mem_nhds
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α] {a b x : α},
a < x → x < b → Set.Ioo a b ∈ nhds x- Defined in
- Mathlib.Topology.Order.OrderClosed
- Cited by
- 27 results in Mathlib
- Foundations
- Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · 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
- Set.Ioostatement · cited by 1,214
- IsOpen.mem_nhdsproof · cited by 470
- OrderClosedTopologystatement and proof · cited by 445
- isOpen_Iooproof · cited by 54
Cited by27
Results whose statement or proof uses this declaration.
- Icc_mem_nhdsproof · cited by 20
- MonotoneOn.ae_differentiableWithinAt_of_memproof · cited by 3
- locallyFinite_Icc_of_tendstoproof · cited by 3
- mem_nhds_iff_exists_Ioo_subset'proof · cited by 3
- Ico_mem_nhdsproof · cited by 3
- isMIntegralCurveOn_Ioo_eqOn_of_contMDiffproof · cited by 2
- ConvexOn.continuousOn_Icoproof · cited by 2
- ConvexOn.continuousOn_Iocproof · cited by 2
- Manifold.pathELength_congr_Iooproof · cited by 2
- Ioc_mem_nhdsproof · cited by 1
- intervalIntegral.continuous_parametric_primitive_of_continuousproof · cited by 1
- isLocalMax_of_deriv_Iooproof · cited by 1