SKolodynski / IsarMathLib

IsarMathLib is a library of formalized mathematics for Isabelle/ZF.
https://isarmathlib.org
Other
17 stars 2 forks source link

Topological group uniformities. Roelcke uniformity. #4

Open dan323 opened 4 years ago

dan323 commented 4 years ago

Proof that the Roelcke uniformity is a uniformity, defined in here for example.

dan323 commented 4 years ago

For the 3rd step, we need this issue

SKolodynski commented 2 years ago

Uniform continuity of the inverse is done with inv_uniform_roelcke, what still remains to be done is the uniform continuity of the group operation.