Submultisets

module trees.submultisets where

open import foundation.embeddings
open import foundation.equivalences
open import foundation.universe-levels

open import trees.multisets

Idea

Given two multisets x and y, we say that x is a submultiset of y if for every z ∈-𝕍 x we have z ∈-𝕍 x ↪ z ∈-𝕍 y.

Definition

Submultisets

is-submultiset-𝕍 : {l : Level} → 𝕍 l → 𝕍 l → UU (lsuc l)
is-submultiset-𝕍 {l} y x = (z : 𝕍 l) → z ∈-𝕍 x → (z ∈-𝕍 x) ↪ (z ∈-𝕍 y)

_⊆-𝕍_ : {l : Level} → 𝕍 l → 𝕍 l → UU (lsuc l)
x ⊆-𝕍 y = is-submultiset-𝕍 y x

Full submultisets

is-full-submultiset-𝕍 : {l : Level} → 𝕍 l → 𝕍 l → UU (lsuc l)
is-full-submultiset-𝕍 {l} y x = (z : 𝕍 l) → z ∈-𝕍 x → (z ∈-𝕍 x) ≃ (z ∈-𝕍 y)

_⊑-𝕍_ : {l : Level} → 𝕍 l → 𝕍 l → UU (lsuc l)
x ⊑-𝕍 y = is-full-submultiset-𝕍 y x