Commit 2023-09-06 23:43 36c3259c

View on Github →

feat: Type synonym for the specialisation order (#6985) Define Specialization α for a topological space α and equip it with the specialisation order. This constitutes a functor from topological spaces to preorders, and T₀ spaces to partial orders.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Specialization.lean

added def Specialization.map

added theorem Specialization.map_comp

added theorem Specialization.map_id

added def Specialization.ofEquiv

added theorem Specialization.ofEquiv_inj

added theorem Specialization.ofEquiv_specializes_ofEquiv

added theorem Specialization.ofEquiv_symm

added theorem Specialization.ofEquiv_toEquiv

added def Specialization.toEquiv

added theorem Specialization.toEquiv_inj

added theorem Specialization.toEquiv_le_toEquiv

added theorem Specialization.toEquiv_ofEquiv

added theorem Specialization.toEquiv_symm

added def Specialization