Theorems · Theorem · order theory
PredOrder.nhds_of_isMax
∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α] [PredOrder α] [NoMinOrder α]
{a : α}, IsMax a → nhds a = pure a- Defined in
- Mathlib.Topology.Order.SuccPred
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 92 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
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
- Filterstatement · cited by 8,121
- nhdsstatement · cited by 5,554
- OrderTopologystatement and proof · cited by 1,355
- IsMaxstatement and proof · cited by 372
- PredOrderstatement and proof · cited by 334
- NoMinOrderstatement and proof · cited by 247
- Order.IsPredPrelimitproof · cited by 93
- Order.isPredLimit_iffproof · cited by 10
- PredOrder.nhds_eq_pureproof · cited by 2
Cited by2
Results whose statement or proof uses this declaration.
- PredOrder.accPt_principalproof · cited by 2
- PredOrder.nhds_topproof · cited by 0