Mathlib Map

Theorems · Theorem · general topology

Topology.IsLower.isUpperSet_of_isClosed

∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsLower α] {s : Set α},
  IsClosed s → IsUpperSet s
Defined in
Mathlib.Topology.Order.LowerUpperTopology
Cited by
1 results in Mathlib
Foundations
Depth 58 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
PreorderTopologicalSpaceTopology.IsLower
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Topology.IsLower.closure_singleton · cited by 1IsLower.closure_singletonSet · cited by 53352SetTopologicalSpace · cited by 24529TopologicalSpacePreorder · cited by 7952PreorderIsClosed · cited by 1639IsClosedIsUpperSet · cited by 148IsUpperSetIsClosed.isOpen_compl · cited by 126IsClosed.isOpen_complTopology.IsLower · cited by 24Topology.IsLowerisLowerSet_compl · cited by 6isLowerSet_complTopology.IsLower.isLowerSet_of_isOpen · cited by 4IsLower.isLowerSet_of_isO…IsLower.isUpperSet_of_isClosedCITED BYCITES

Cites9

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.