Subsemigroup lemmas

This file contains lemmas about the lattice of Subsemigroups.

theorem Subsemigroup.coe_iSup_eq_iUnion_finset_coe_biSup {M : Type u_1} [Mul M] {ι : Type u_2} (S : ι → Subsemigroup M) : ↑(⨆ (i : ι), S i) = ⋃ (s : Finset ι), ↑(⨆ i ∈ s, S i)

theorem AddSubsemigroup.coe_iSup_eq_iUnion_finset_coe_biSup {M : Type u_1} [Add M] {ι : Type u_2} (S : ι → AddSubsemigroup M) : ↑(⨆ (i : ι), S i) = ⋃ (s : Finset ι), ↑(⨆ i ∈ s, S i)