Subsets of abelian groups

Content created by Egbert Rijke, Fredrik Bakke and Maša Žaucer.

Created on 2023-06-08.
Last modified on 2023-06-08.

module group-theory.subsets-abelian-groups where
Imports 
open import foundation.sets
open import foundation.universe-levels

open import group-theory.abelian-groups
open import group-theory.subsets-groups

Idea

A subset of an abelian group A is a subtype of the underlying type of A.

Definitions

Subsets of abelian groups

subset-Ab :
  (l : Level) {l1 : Level} (A : Ab l1) → UU ((lsuc l) ⊔ l1)
subset-Ab l A = subset-Group l (group-Ab A)

is-set-subset-Ab :
  (l : Level) {l1 : Level} (A : Ab l1) → is-set (subset-Ab l A)
is-set-subset-Ab l A = is-set-subset-Group (group-Ab A)

Recent changes