# Multisubsets

Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke and Eléonore Mangel.

Created on 2022-04-08.

module foundation.multisubsets where

Imports
open import elementary-number-theory.natural-numbers

open import foundation.dependent-pair-types
open import foundation.images
open import foundation.negated-equality
open import foundation.universe-levels

open import foundation-core.fibers-of-maps
open import foundation-core.sets

open import univalent-combinatorics.finite-types


## Idea

A multisubset of a given set U is a type B equipped with a function f : B → U

## Definition

module _
{l1 : Level} (l2 : Level)
where

multisubset : Set l1 → UU (l1 ⊔ lsuc l2)
multisubset U = Σ (UU l2) (λ B → B → type-Set U)

is-locally-finite-multisubset :
(U : Set l1) → multisubset U → UU (l1 ⊔ l2)
is-locally-finite-multisubset U (pair B f) =
(x : type-Set U) → is-finite (fiber f x)

is-finite-multisubset :
(U : Set l1) → multisubset U → UU (l1 ⊔ l2)
is-finite-multisubset U (pair B f) = is-finite (im f)

module _
{l1 : Level}
where

locally-finite-multisubset : Set l1 → UU l1
locally-finite-multisubset U = type-Set U → ℕ

support-locally-finite-multisubset :
(U : Set l1) → locally-finite-multisubset U → UU l1
support-locally-finite-multisubset U μ =
Σ (type-Set U) (λ x → μ x ≠ 0)

is-finite-locally-finite-multisubset :
(U : Set l1) → locally-finite-multisubset U → UU l1
is-finite-locally-finite-multisubset U μ =
is-finite (support-locally-finite-multisubset U μ)