Mathlib Changelog
Changelog
About
Github
Commit
2022-11-09 17:39
1499a80b
View on Github →
feat(topology/uniform_space): ulift as a uniform equiv (
#17451
)
Estimated changes
Modified
src/topology/algebra/module/basic.lean
added
theorem
continuous_linear_equiv.prod_symm
added
def
continuous_linear_equiv.ulift
Modified
src/topology/uniform_space/basic.lean
Modified
src/topology/uniform_space/equiv.lean
added
def
uniform_equiv.pi_fin_two
added
def
uniform_equiv.ulift
deleted
def
uniform_equiv.{u}
Modified
src/topology/uniform_space/uniform_embedding.lean