Theorems · Theorem · general topology
exists_Ioc_subset_of_mem_nhds
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {a : α} {s : Set α},
s ∈ nhds a → (∃ l, l < a) → ∃ l < a, Set.Ioc l a ⊆ s- Defined in
- Mathlib.Topology.Order.Basic
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 72 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.
- 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 and proof · cited by 5,554
- OrderTopologystatement and proof · cited by 1,355
- Set.Iocstatement · cited by 971
- Filter.HasBasis.mem_iffproof · cited by 193
- nhdsWithin_le_nhdsproof · cited by 145
- nhdsLE_basis_of_exists_ltproof · cited by 5
Cited by8
Results whose statement or proof uses this declaration.
- Antitone.map_limsSup_of_continuousAtproof · cited by 6
- ContinuousAt.comp_lowerSemicontinuousWithinAtproof · cited by 4
- LowerSemicontinuousWithinAt.add'proof · cited by 4
- mem_nhds_iff_exists_Ioo_subset'proof · cited by 3
- countable_setOfPred_covBy_rightproof · cited by 3
- IsOpen.exists_Ioo_subsetproof · cited by 1
- exists_Ioc_subset_of_mem_nhds'proof · cited by 0
- continuousWithinAt_iff_lower_upperSemicontinuousWithinAtproof · cited by 0