Re: [mizar] Union of two subgroups

[Adam Naumowicz <adamn@math.uwb.edu.pl>]

Dear Victor,

On Mon, 16 Nov 2020, Victor Makarov wrote:

> Dear All:
>
> I cannot find in MML a theorem that the union of two subgroups is  a
> subgroup iff  one of the subgroups is a subset of the other subgroup.
>
> The same question about the product of two subgroups H and K:
>
> H*K is a subgroup iff H*K = K*H.

This may not be exactly what you want, but have you checked these 
theorems:

theorem :: GROUP_4:50
  H1 "\/" H2 = gr(H1 * H2);

theorem :: GROUP_4:51
  H1 * H2 = H2 * H1 implies the carrier of H1 "\/" H2 = H1 * H2;

?

Best regards,

Adam Naumowicz

===========================================================================
Division of Programming and Formal Methods   Fax: +48(85)738-83-33
Institute of Computer Science                Tel: +48(85)738-83-06 (office)
University of Bialystok                      E-mail: adamn@mizar.org
Ciolkowskiego 1M, 15-245 Bialystok, Poland   http://math.uwb.edu.pl/~adamn/
===========================================================================