Commit 2024-05-26 14:25 84e22426

View on Github →

feat: the largest T2 quotient of a topological space. (#13061)

Estimated changes

Modified Mathlib/Data/Setoid/Basic.lean

added def Setoid.map_of_le

added def Setoid.map_sInf

added theorem Setoid.quotient_mk_sInf_eq

added theorem Setoid.sInf_equiv

Modified Mathlib/Topology/Constructions.lean

added theorem continuous_map_of_le

added theorem continuous_map_sInf

Modified Mathlib/Topology/Separation.lean

added theorem t2Quotient.compatible

added theorem t2Quotient.continuous_lift

added theorem t2Quotient.continuous_mk

added def t2Quotient.lift

added theorem t2Quotient.lift_mk

added def t2Quotient.mk

added theorem t2Quotient.mk_eq

added theorem t2Quotient.surjective_mk

added theorem t2Quotient.unique_lift

added def t2Quotient

added def t2Setoid

Modified scripts/style-exceptions.txt