Mathlib v3 is deprecated. Go to Mathlib v4

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