Mathlib Map

Theorems · Theorem · order theory

PredOrder.nhds_eq_pure

∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α] [PredOrder α] [NoMinOrder α]
  {a : α}, nhds a = pure a ↔ ¬Order.IsPredLimit a
Defined in
Mathlib.Topology.Order.SuccPred
Cited by
2 results in Mathlib
Foundations
Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
LinearOrderTopologicalSpaceOrderTopologyPredOrderNoMinOrder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

PredOrder.nhds_of_isMax · cited by 2PredOrder.nhds_of_isMaxPredOrder.isOpen_iff · cited by 0PredOrder.isOpen_iffTopologicalSpace · cited by 24529TopologicalSpaceLinearOrder · cited by 8572LinearOrderFilter · cited by 8121Filternhds · cited by 5554nhdsOrderTopology · cited by 1355OrderTopologyPredOrder · cited by 334PredOrderNoMinOrder · cited by 247NoMinOrderOrder.IsPredLimit · cited by 60Order.IsPredLimitisOpen_singleton_iff_nhds_eq_pure · cited by 9isOpen_singleton_iff_nhds…PredOrder.isOpen_singleton_iff · cited by 2PredOrder.isOpen_singleto…PredOrder.nhds_eq_pureCITED BYCITES

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by2

Results whose statement or proof uses this declaration.