IsarMathLib version 1.15.0: comparison with Mizar

[CoghettoR]

A union of two subgroups is a subgroup iff one of the subgroups is a subset of the other subgroup. If H,K are subgroups then H⋅K is a subgroup iff H⋅K=K⋅H.

Your code is smaller!

Can you tell me, where in the IsarMathLib, I could find the equivalent of the following Mizar/MML proposal ?

theorem Th56: :: GROUP_2:56 for G1, G2, G3 being Group st G1 is Subgroup of G2 & G2 is Subgroup of G3 holds G1 is Subgroup of G3 Source: http://mizar.uwb.edu.pl/version/current/html/group_2.html

This would allow me to understand the consequences of the definition of subgroup, defined in IsarMathLib.

Regards, Roland

[SKolodynski]

Currently IsarMathLib does not have such theorem. I will add some analogue of this before the next release. The statement will look a bit different because of the way the notions of being a group and being a subgroup are defined in IsarMathLib as predicates on two sets (as you have noticed probably).

[CoghettoR]

Additionally, a topological space in IsarMathLib is defined without the need for the topology carrier.

One can notice here that since we always have⋃T=X, the set on which the topology is defined (the ”carrier” of the topology) can always be constructed from the topology itself and is superfluous in the definition. Source: https://skolodynski.github.io/IsarMathLib/IsarMathLib/outline.pdf, p 321, ""50.1 Basic definitions and properties"

Is it also possible to define the group without having to introduce the carrier? (of course, the carrier is reconstructed from the operation of the group).

Is it possible or useful for you to also generalize the definition of "IsAtopologicalGroup "IsAtopologicalGroup(T,f) ≡ (T {is a topology}) ∧ IsAgroup(⋃T,f) ∧ IsContinuous(ProductTopology(T,T),T,f) ∧ IsContinuous(T,T,GroupInv(⋃T,f))" and for example to obtain "a set S is a topological group if FUN1(S) is a group & FUN2(S) is a topological space and the carrier of FUN1(S) = Union(PROJ2(S))". Of course if S is of the form (G,T) this is trivial but in the case where S is a set which is not necessarily a couple.

The first aim is to conclude whether or not there is also superfluous information in the group or topological group definitions.

This may be useful in the case of structure representation, for example in the Grothendieck universes. Even if IsarMathLib does not contain the great cardinals, it is still possible to explore the possibility of finding structures of the type group, topology, or topological group, or other combinations of structures other than in the classical form of a couple set (the carrier, the topology) or (the carrier, the operation of monoid), or (the carrier, the group operation, the topology). etc.

[SKolodynski]

It is possible to define the notion of being a group as a predicate on only one set - the one representing the group operation. I was thinking of doing that 16 years ago when I was writing the definition of IsAgroup predicate and decided against it as it would make many proofs longer and less familiar for mathematicians. It is a trade-off that I made a couple of times, most recently in the definition of r is a lattice on L in the Lattice_ZF theory. Whether that trade-off is worth it is a matter of taste. If you feel like it you can try a parallel development with a different definition of IsAgroup. If you name it differently and with some theorem stating the equivalence of the new definition with the current one it should be possible to reference the existing group theory material in the new development.

[SKolodynski]

I have added the theorem about transitivity of subgroups as the subgroup_transitive lemma.