Mathlib Map

Theorems · Definition · general topology

Specialization

Type u_1 → Type u_1

Type synonym for a topological space considered with its specialisation order.

Defined in
Mathlib.Topology.Specialization
Cited by
15 results in Mathlib
Foundations
Depth 0 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Specialization.ofEquiv · cited by 7Specialization.ofEquivSpecialization.toEquiv · cited by 7Specialization.toEquivtopToPreord · cited by 5topToPreordSpecialization.map · cited by 3Specialization.maporderIsoSpecializationWithUpperSetTopology · cited by 1orderIsoSpecializationWit…Specialization.isOpen_toEquiv_preimage · cited by 1Specialization.isOpen_toE…homeoWithUpperSetTopologyorderIso · cited by 1homeoWithUpperSetTopology…topToPreord_map · cited by 0topToPreord_maptopToPreord_obj_coe · cited by 0topToPreord_obj_coealexDiscEquivPreord_counitIso · cited by 0alexDiscEquivPreord_couni…Specialization.isUpperSet_ofEquiv_preimage · cited by 0Specialization.isUpperSet…Specialization.map_comp · cited by 0Specialization.map_compSpecialization.map_id · cited by 0Specialization.map_idSpecialization.ofEquiv_inj · cited by 0Specialization.ofEquiv_injSpecialization.ofEquiv_specializes_ofEquiv · cited by 0Specialization.ofEquiv_sp…SpecializationCITED BYCITES

Cites0

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

Nothing in Mathlib beyond the foundations.

Cited by22

Results whose statement or proof uses this declaration.