search

SKolodynski / IsarMathLib

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

side uniformities for topological groups #3

Closed dan323 closed 4 years ago

dan323 commented 4 years ago

Here is the proof for the existence of the left and right uniformities for topological groups.

dan323 commented 4 years ago

I did not know what branch to merge to.

SKolodynski commented 4 years ago

Pull requests against master are ok, I will merge each into its own branch anyway.

SKolodynski commented 4 years ago

I am thinking maybe it would be more convenient if I create a special branch for you to send pull requests to? I have to read a bit how this is typically done.

SKolodynski commented 4 years ago

Turns out I can check out your pull request locally without creating any new branches on GitHub. So, for the IsarMathLib scale sending pull requests to master is fine.

SKolodynski commented 4 years ago

After merging I got *** Undefined fact: "group0_5_L1" (line 281 of "~/Projects/IsarMathLib/git/IsarMathLib/TopologicalGroup_ZF.thy")

Must be something in your fork that I changed in mine. Can you give me some string from the source of the group0_5_L1 lemma in your fork so that I can search how is it called now in mine?

dan323 commented 4 years ago

lemma (in group0) group0_5_L1: assumes A1: "g\G" shows "RightTranslation(G,P,g) : G\G" and "LeftTranslation(G,P,g) : G\G" proof - from A1 have "\a\G. a\g \ G" and "\a\G. g\a \ G" using group_oper_assocA apply_funtype by auto then show "RightTranslation(G,P,g) : G\G" "LeftTranslation(G,P,g) : G\G" using RightTranslation_def LeftTranslation_def func1_1_L11A by auto qed