Re: Union of two subgroups

Victor Makarov <[email protected]> Tue, 17 Nov 2020 22:13:46 -0500
Newsgroups gmane.comp.mathematics.mizar
Message-ID <CAHZyMifLCeaA-FYamk3-GNCmtBA9r6PwbLHu2SvVOrJ-5+qt7A@mail.gmail.com>
Thanks, I'll check them out.

On Tue, Nov 17, 2020 at 7:51 AM Adam Naumowicz <[email protected]>
wrote:

> 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: [email protected]
> Ciolkowskiego 1M, 15-245 Bialystok, Poland
> http://math.uwb.edu.pl/~adamn/
> ===========================================================================
>
>