Mathlib Map

Theorems · Theorem · general topology

PredOrder.nhdsLE

∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIicTopology α] {b : α} [PredOrder α],
  nhdsWithin b (Set.Iic b) = pure b
Defined in
Mathlib.Topology.Order.OrderClosed
Cited by
1 results in Mathlib
Foundations
Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
TopologicalSpaceLinearOrderClosedIicTopologyPredOrder
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

DiscreteTopology.of_predOrder_succOrder · cited by 1DiscreteTopology.of_predO…Set · cited by 53352SetTopologicalSpace · cited by 24529TopologicalSpaceLinearOrder · cited by 8572LinearOrderFilter · cited by 8121FilternhdsWithin · cited by 1912nhdsWithinSet.Iio · cited by 1166Set.IioSet.Iic · cited by 1111Set.IicPredOrder · cited by 334PredOrderClosedIicTopology · cited by 115ClosedIicTopologysup_bot_eq · cited by 31sup_bot_eqnhdsWithin_insert · cited by 13nhdsWithin_insertSet.Iio_insert · cited by 5Set.Iio_insertPredOrder.nhdsLT · cited by 3PredOrder.nhdsLTPredOrder.nhdsLECITED BYCITES

Cites13

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

Cited by1

Results whose statement or proof uses this declaration.