Theorems · Theorem · general topology
nhdsGE_basis_of_exists_gt
∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {a : α},
(∃ u, a < u) → (nhdsWithin a (Set.Ici a)).HasBasis (fun u => a < u) fun u => Set.Ico a u- Defined in
- Mathlib.Topology.Order.Basic
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 67 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
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
- LinearOrderstatement and proof · cited by 8,572
- nhdsWithinstatement · cited by 1,912
- OrderTopologystatement and proof · cited by 1,355
- Set.Icistatement · cited by 1,070
- Set.Icostatement · cited by 799
- Filter.HasBasisstatement · cited by 604
- min_le_leftproof · cited by 105
- min_le_rightproof · cited by 88
- lt_minproof · cited by 69
- Set.Ico_subset_Ico_rightproof · cited by 6
- Filter.hasBasis_biInf_principalproof · cited by 5
Cited by6
Results whose statement or proof uses this declaration.
- exists_Ico_subset_of_mem_nhdsproof · cited by 7
- nhds_bot_basisproof · cited by 6
- PredOrder.hasBasis_nhds_Ico_of_exists_gtproof · cited by 4
- TFAE_mem_nhdsGEproof · cited by 3
- exists_Icc_mem_subset_of_mem_nhdsGEproof · cited by 2
- nhdsGE_basisproof · cited by 1