Mathlib Map

Theorems · Theorem · general topology

CovBy.nhdsGE

∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIciTopology α] {a b : α},
  b ⋖ a → nhdsWithin b (Set.Ici b) = pure b
Defined in
Mathlib.Topology.Order.OrderClosed
Cited by
0 results in Mathlib
Foundations
Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
TopologicalSpaceLinearOrderClosedIciTopology
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Set · cited by 53352SetTopologicalSpace · cited by 24529TopologicalSpaceLinearOrder · cited by 8572LinearOrderFilter · cited by 8121FilternhdsWithin · cited by 1912nhdsWithinSet.Ioi · cited by 1463Set.IoiSet.Ici · cited by 1070Set.IciCovBy · cited by 290CovByClosedIciTopology · cited by 156ClosedIciTopologysup_bot_eq · cited by 31sup_bot_eqnhdsWithin_insert · cited by 13nhdsWithin_insertSet.Ioi_insert · cited by 5Set.Ioi_insertCovBy.nhdsGT · cited by 4CovBy.nhdsGTCovBy.nhdsGECITED BYCITES

Cites13

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

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.