Mathlib.Data.Multiset.ZeroCons

Multiset.zero definition

: Multiset α

Full source

/-- `0 : Multiset α` is the empty set -/
protected def zero : Multiset α :=
  @nil α

Empty multiset

Informal description

The empty multiset, denoted by $0$, is the multiset containing no elements of type $\alpha$.

Multiset.instZero instance

: Zero (Multiset α)

Full source

instance : Zero (Multiset α) :=
  ⟨Multiset.zero⟩

The Zero Multiset

Informal description

The empty multiset $0$ is the zero element of the type `Multiset α`.

Multiset.instEmptyCollection instance

: EmptyCollection (Multiset α)

Full source

instance : EmptyCollection (Multiset α) :=
  ⟨0⟩

Empty Multiset as Empty Collection

Informal description

The empty multiset $0$ is the empty collection of the type `Multiset α`.

Multiset.inhabitedMultiset instance

: Inhabited (Multiset α)

Full source

instance inhabitedMultiset : Inhabited (Multiset α) :=
  ⟨0⟩

Inhabitedness of Multisets

Informal description

The type `Multiset α` is inhabited, with the empty multiset $0$ as its default element.

Multiset.instUniqueOfIsEmpty instance

[IsEmpty α] : Unique (Multiset α)

Full source

instance [IsEmpty α] : Unique (Multiset α) where
  default := 0
  uniq := by rintro ⟨_ | ⟨a, l⟩⟩; exacts [rfl, isEmptyElim a]

Uniqueness of Empty Multisets

Informal description

For any type $\alpha$ that is empty (i.e., has no elements), the multiset over $\alpha$ is unique (has exactly one element, the empty multiset).

Multiset.coe_nil theorem

: (@nil α : Multiset α) = 0

Full source

@[simp]
theorem coe_nil : (@nil α : Multiset α) = 0 :=
  rfl

Empty List as Zero Multiset

Informal description

The empty list, when interpreted as a multiset, is equal to the zero multiset, i.e., $[] = 0$ in `Multiset α`.

Multiset.empty_eq_zero theorem

: (∅ : Multiset α) = 0

Full source

@[simp]
theorem empty_eq_zero : (∅ : Multiset α) = 0 :=
  rfl

Empty Multiset Equals Zero Multiset

Informal description

The empty multiset $\emptyset$ is equal to the zero multiset $0$ in the type `Multiset α`.

Multiset.coe_eq_zero theorem

(l : List α) : (l : Multiset α) = 0 ↔ l = []

Full source

@[simp]
theorem coe_eq_zero (l : List α) : (l : Multiset α) = 0 ↔ l = [] :=
  Iff.trans coe_eq_coe perm_nil

List-to-Multiset Conversion Yields Zero Multiset if and Only if List is Empty

Informal description

For any list $l$ of elements of type $\alpha$, the multiset obtained from $l$ is equal to the empty multiset $0$ if and only if $l$ is the empty list $[]$.

Multiset.coe_eq_zero_iff_isEmpty theorem

(l : List α) : (l : Multiset α) = 0 ↔ l.isEmpty

Full source

theorem coe_eq_zero_iff_isEmpty (l : List α) : (l : Multiset α) = 0 ↔ l.isEmpty :=
  Iff.trans (coe_eq_zero l) isEmpty_iff.symm

Empty List to Multiset Conversion Criterion

Informal description

For any list $l$ of elements of type $\alpha$, the multiset obtained from $l$ is equal to the empty multiset $0$ if and only if $l$ is empty (i.e., $l.\text{isEmpty}$ holds).

Multiset.cons definition

(a : α) (s : Multiset α) : Multiset α

Full source

/-- `cons a s` is the multiset which contains `s` plus one more instance of `a`. -/
def cons (a : α) (s : Multiset α) : Multiset α :=
  Quot.liftOn s (fun l => (a :: l : Multiset α)) fun _ _ p => Quot.sound (p.cons a)

Multiset insertion

Informal description

Given an element $a$ of type $\alpha$ and a multiset $s$ over $\alpha$, the operation $\text{cons}(a, s)$ returns a new multiset that contains all elements of $s$ plus one additional occurrence of $a$.

Multiset.term_::ₘ_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc Multiset.cons]
infixr:67 " ::ₘ " => Multiset.cons

Multiset cons notation

Informal description

The notation `a ::ₘ s` represents the multiset obtained by adding one occurrence of the element `a` to the multiset `s`. This is the multiset analog of the list cons operation `::`.

Multiset.instInsert instance

: Insert α (Multiset α)

Full source

instance : Insert α (Multiset α) :=
  ⟨cons⟩

Insertion Operation for Multisets

Informal description

For any type $\alpha$, there is an insertion operation that allows inserting an element into a multiset over $\alpha$.

Multiset.insert_eq_cons theorem

(a : α) (s : Multiset α) : insert a s = a ::ₘ s

Full source

@[simp]
theorem insert_eq_cons (a : α) (s : Multiset α) : insert a s = a ::ₘ s :=
  rfl

Insertion Equivalence to Multiset Cons: $\text{insert}(a, s) = a ::ₘ s$

Informal description

For any element $a$ of type $\alpha$ and any multiset $s$ over $\alpha$, the insertion of $a$ into $s$ is equal to the multiset obtained by adding one occurrence of $a$ to $s$, i.e., $\text{insert}(a, s) = a ::ₘ s$.

Multiset.cons_coe theorem

(a : α) (l : List α) : (a ::ₘ l : Multiset α) = (a :: l : List α)

Full source

@[simp]
theorem cons_coe (a : α) (l : List α) : (a ::ₘ l : Multiset α) = (a :: l : List α) :=
  rfl

Multiset Insertion Equivalence to List Prepending

Informal description

For any element $a$ of type $\alpha$ and any list $l$ of elements of type $\alpha$, the multiset obtained by inserting $a$ into the multiset corresponding to $l$ is equal to the multiset corresponding to the list obtained by prepending $a$ to $l$. In symbols: $a ::ₘ (l : \text{Multiset} \alpha) = (a :: l : \text{List} \alpha)$.

Multiset.cons_inj_left theorem

{a b : α} (s : Multiset α) : a ::ₘ s = b ::ₘ s ↔ a = b

Full source

@[simp]
theorem cons_inj_left {a b : α} (s : Multiset α) : a ::ₘ sa ::ₘ s = b ::ₘ s ↔ a = b :=
  ⟨Quot.inductionOn s fun l e =>
      have : [a] ++ l ~ [b] ++ l := Quotient.exact e
      singleton_perm_singleton.1 <| (perm_append_right_iff _).1 this,
    congr_arg (· ::ₘ _)⟩

Left Injectivity of Multiset Insertion: $a ::ₘ s = b ::ₘ s ↔ a = b$

Informal description

For any elements $a$ and $b$ of type $\alpha$ and any multiset $s$ over $\alpha$, the equality $a ::ₘ s = b ::ₘ s$ holds if and only if $a = b$.

Multiset.cons_inj_right theorem

(a : α) : ∀ {s t : Multiset α}, a ::ₘ s = a ::ₘ t ↔ s = t

Full source

@[simp]
theorem cons_inj_right (a : α) : ∀ {s t : Multiset α}, a ::ₘ sa ::ₘ s = a ::ₘ t ↔ s = t := by
  rintro ⟨l₁⟩ ⟨l₂⟩; simp

Right Injectivity of Multiset Insertion: $a \mathbin{::ₘ} s = a \mathbin{::ₘ} t \leftrightarrow s = t$

Informal description

For any element $a$ of type $\alpha$ and any multisets $s$ and $t$ over $\alpha$, the equality $a \mathbin{::ₘ} s = a \mathbin{::ₘ} t$ holds if and only if $s = t$.

Multiset.induction theorem

{p : Multiset α → Prop} (empty : p 0) (cons : ∀ (a : α) (s : Multiset α), p s → p (a ::ₘ s)) : ∀ s, p s

Full source

@[elab_as_elim]
protected theorem induction {p : Multiset α → Prop} (empty : p 0)
    (cons : ∀ (a : α) (s : Multiset α), p s → p (a ::ₘ s)) : ∀ s, p s := by
  rintro ⟨l⟩; induction l with | nil => exact empty | cons _ _ ih => exact cons _ _ ih

Induction Principle for Multisets: Base Case and Insertion Step Implies Universality

Informal description

For any predicate $p$ on multisets over a type $\alpha$, if $p$ holds for the empty multiset $0$, and for any element $a \in \alpha$ and multiset $s$, $p(s)$ implies $p(a \mathbin{::ₘ} s)$, then $p$ holds for all multisets $s$.

Multiset.induction_on theorem

 {p : Multiset α → Prop} (s : Multiset α) (empty : p 0) (cons : ∀ (a : α) (s : Multiset α), p s → p (a ::ₘ s)) : p s

Full source

@[elab_as_elim]
protected theorem induction_on {p : Multiset α → Prop} (s : Multiset α) (empty : p 0)
    (cons : ∀ (a : α) (s : Multiset α), p s → p (a ::ₘ s)) : p s :=
  Multiset.induction empty cons s

Induction Principle for Multisets Applied to a Specific Multiset

Informal description

For any predicate $p$ on multisets over a type $\alpha$, given a multiset $s$, if $p$ holds for the empty multiset $0$, and for any element $a \in \alpha$ and multiset $s'$, $p(s')$ implies $p(a \mathbin{::ₘ} s')$, then $p$ holds for $s$.

Multiset.cons_swap theorem

(a b : α) (s : Multiset α) : a ::ₘ b ::ₘ s = b ::ₘ a ::ₘ s

Full source

theorem cons_swap (a b : α) (s : Multiset α) : a ::ₘ b ::ₘ s = b ::ₘ a ::ₘ s :=
  Quot.inductionOn s fun _ => Quotient.sound <| Perm.swap _ _ _

Commutativity of Multiset Insertion: $a ::ₘ b ::ₘ s = b ::ₘ a ::ₘ s$

Informal description

For any elements $a$ and $b$ of type $\alpha$ and any multiset $s$ over $\alpha$, the multisets $a ::ₘ (b ::ₘ s)$ and $b ::ₘ (a ::ₘ s)$ are equal. In other words, the order of inserting two distinct elements into a multiset does not affect the resulting multiset.

Multiset.rec definition

 (C_0 : C 0) (C_cons : ∀ a m, C m → C (a ::ₘ m))
  (C_cons_heq : ∀ a a' m b, HEq (C_cons a (a' ::ₘ m) (C_cons a' m b)) (C_cons a' (a ::ₘ m) (C_cons a m b)))
  (m : Multiset α) : C m

Full source

/-- Dependent recursor on multisets.
TODO: should be @[recursor 6], but then the definition of `Multiset.pi` fails with a stack
overflow in `whnf`.
-/
protected
def rec (C_0 : C 0) (C_cons : ∀ a m, C m → C (a ::ₘ m))
    (C_cons_heq :
      ∀ a a' m b, HEq (C_cons a (a' ::ₘ m) (C_cons a' m b)) (C_cons a' (a ::ₘ m) (C_cons a m b)))
    (m : Multiset α) : C m :=
  Quotient.hrecOn m (@List.rec α (fun l => C ⟦l⟧) C_0 fun a l b => C_cons a ⟦l⟧ b) fun _ _ h =>
    h.rec_heq
      (fun hl _ ↦ by congr 1; exact Quot.sound hl)
      (C_cons_heq _ _ ⟦_⟧ _)

Dependent recursor for multisets

Informal description

The dependent recursor for multisets, which allows defining a function on all multisets by specifying its value on the empty multiset $0$ and how to extend it when adding an element $a$ to a multiset $m$. The function must satisfy a coherence condition ensuring that the result is independent of the order in which elements are added to the multiset.

Multiset.recOn definition

 (m : Multiset α) (C_0 : C 0) (C_cons : ∀ a m, C m → C (a ::ₘ m))
  (C_cons_heq : ∀ a a' m b, HEq (C_cons a (a' ::ₘ m) (C_cons a' m b)) (C_cons a' (a ::ₘ m) (C_cons a m b))) : C m

Full source

/-- Companion to `Multiset.rec` with more convenient argument order. -/
@[elab_as_elim]
protected
def recOn (m : Multiset α) (C_0 : C 0) (C_cons : ∀ a m, C m → C (a ::ₘ m))
    (C_cons_heq :
      ∀ a a' m b, HEq (C_cons a (a' ::ₘ m) (C_cons a' m b)) (C_cons a' (a ::ₘ m) (C_cons a m b))) :
    C m :=
  Multiset.rec C_0 C_cons C_cons_heq m

Dependent recursor for multisets with convenient argument order

Informal description

Given a multiset $m$ over type $\alpha$, a base case value $C_0$ for the empty multiset $0$, and a step function $C_{\text{cons}}$ that extends a computation from a multiset $m$ to $a ::ₘ m$ for any element $a$, the function `Multiset.recOn` computes a value of type $C m$. The step function must satisfy a coherence condition ensuring the result is independent of the order in which elements are added to the multiset.

Multiset.recOn_0 theorem

: @Multiset.recOn α C (0 : Multiset α) C_0 C_cons C_cons_heq = C_0

Full source

@[simp]
theorem recOn_0 : @Multiset.recOn α C (0 : Multiset α) C_0 C_cons C_cons_heq = C_0 :=
  rfl

Recursor Base Case for Empty Multiset: $\text{recOn}(0) = C_0$

Informal description

For any type $\alpha$ and any dependent type family $C$ on multisets over $\alpha$, the application of the dependent recursor `Multiset.recOn` to the empty multiset $0$ with base case value $C_0$ and step function $C_{\text{cons}}$ (satisfying the coherence condition) yields $C_0$. In other words, the recursion principle applied to the empty multiset returns the base case value.

Multiset.recOn_cons theorem

(a : α) (m : Multiset α) : (a ::ₘ m).recOn C_0 C_cons C_cons_heq = C_cons a m (m.recOn C_0 C_cons C_cons_heq)

Full source

@[simp]
theorem recOn_cons (a : α) (m : Multiset α) :
    (a ::ₘ m).recOn C_0 C_cons C_cons_heq = C_cons a m (m.recOn C_0 C_cons C_cons_heq) :=
  Quotient.inductionOn m fun _ => rfl

Recursor Step Case for Multiset Insertion: $\text{recOn}(a ::ₘ m) = C_{\text{cons}}(a, m, \text{recOn}(m))$

Informal description

For any element $a$ of type $\alpha$ and any multiset $m$ over $\alpha$, the application of the dependent recursor `recOn` to the multiset $a ::ₘ m$ (obtained by adding one occurrence of $a$ to $m$) with base case value $C_0$ and step function $C_{\text{cons}}$ (satisfying the coherence condition) is equal to $C_{\text{cons}}$ applied to $a$, $m$, and the result of applying `recOn` to $m$ with the same arguments.

Multiset.mem_cons theorem

{a b : α} {s : Multiset α} : a ∈ b ::ₘ s ↔ a = b ∨ a ∈ s

Full source

@[simp]
theorem mem_cons {a b : α} {s : Multiset α} : a ∈ b ::ₘ sa ∈ b ::ₘ s ↔ a = b ∨ a ∈ s :=
  Quot.inductionOn s fun _ => List.mem_cons

Membership in Multiset After Insertion: $a \in b ::ₘ s \leftrightarrow a = b \lor a \in s$

Informal description

For any elements $a, b$ of type $\alpha$ and any multiset $s$ over $\alpha$, the element $a$ is in the multiset $b ::ₘ s$ (obtained by adding one occurrence of $b$ to $s$) if and only if either $a = b$ or $a$ is already in $s$.

Multiset.mem_cons_of_mem theorem

{a b : α} {s : Multiset α} (h : a ∈ s) : a ∈ b ::ₘ s

Full source

theorem mem_cons_of_mem {a b : α} {s : Multiset α} (h : a ∈ s) : a ∈ b ::ₘ s :=
  mem_cons.2 <| Or.inr h

Membership Preservation in Multiset Insertion: $a \in s \to a \in b ::ₘ s$

Informal description

For any elements $a, b$ of type $\alpha$ and any multiset $s$ over $\alpha$, if $a$ is an element of $s$, then $a$ is also an element of the multiset obtained by adding one occurrence of $b$ to $s$ (denoted $b ::ₘ s$).

Multiset.mem_cons_self theorem

(a : α) (s : Multiset α) : a ∈ a ::ₘ s

Full source

theorem mem_cons_self (a : α) (s : Multiset α) : a ∈ a ::ₘ s :=
  mem_cons.2 (Or.inl rfl)

Self-Membership in Multiset Insertion: $a \in a ::ₘ s$

Informal description

For any element $a$ of type $\alpha$ and any multiset $s$ over $\alpha$, the element $a$ is contained in the multiset obtained by adding one occurrence of $a$ to $s$, i.e., $a \in a ::ₘ s$.

Multiset.forall_mem_cons theorem

{p : α → Prop} {a : α} {s : Multiset α} : (∀ x ∈ a ::ₘ s, p x) ↔ p a ∧ ∀ x ∈ s, p x

Full source

theorem forall_mem_cons {p : α → Prop} {a : α} {s : Multiset α} :
    (∀ x ∈ a ::ₘ s, p x) ↔ p a ∧ ∀ x ∈ s, p x :=
  Quotient.inductionOn' s fun _ => List.forall_mem_cons

Universal Quantifier over Multiset Insertion: $(\forall x \in a ::ₘ s, p(x)) \leftrightarrow p(a) \land (\forall x \in s, p(x))$

Informal description

For any predicate $p$ on elements of type $\alpha$, an element $a$ of type $\alpha$, and a multiset $s$ over $\alpha$, the following are equivalent: 1. Every element in the multiset obtained by adding $a$ to $s$ (denoted $a ::ₘ s$) satisfies $p$. 2. The element $a$ satisfies $p$, and every element in $s$ satisfies $p$. In symbols: $$(\forall x \in a ::ₘ s, p(x)) \leftrightarrow p(a) \land (\forall x \in s, p(x))$$

Multiset.exists_cons_of_mem theorem

{s : Multiset α} {a : α} : a ∈ s → ∃ t, s = a ::ₘ t

Full source

theorem exists_cons_of_mem {s : Multiset α} {a : α} : a ∈ s → ∃ t, s = a ::ₘ t :=
  Quot.inductionOn s fun l (h : a ∈ l) =>
    let ⟨l₁, l₂, e⟩ := append_of_mem h
    e.symm ▸ ⟨(l₁ ++ l₂ : List α), Quot.sound perm_middle⟩

Decomposition of Multiset Membership: $a \in s \implies \exists t, s = a ::ₘ t$

Informal description

For any multiset $s$ over a type $\alpha$ and any element $a \in \alpha$, if $a$ is an element of $s$, then there exists a multiset $t$ such that $s$ can be expressed as $a$ cons $t$ (i.e., $s = a ::ₘ t$).

Multiset.not_mem_zero theorem

(a : α) : a ∉ (0 : Multiset α)

Full source

@[simp]
theorem not_mem_zero (a : α) : a ∉ (0 : Multiset α) :=
  List.not_mem_nil

No Element in Empty Multiset: $a \notin 0$

Informal description

For any element $a$ of type $\alpha$, $a$ is not a member of the empty multiset $0$.

Multiset.exists_mem_of_ne_zero theorem

{s : Multiset α} : s ≠ 0 → ∃ a : α, a ∈ s

Full source

theorem exists_mem_of_ne_zero {s : Multiset α} : s ≠ 0 → ∃ a : α, a ∈ s :=
  Quot.inductionOn s fun l hl =>
    match l, hl with
    | [], h => False.elim <| h rfl
    | a :: l, _ => ⟨a, by simp⟩

Nonempty Multiset Contains an Element

Informal description

For any nonempty multiset $s$ (i.e., $s \neq 0$), there exists an element $a \in \alpha$ such that $a$ is a member of $s$.

Multiset.empty_or_exists_mem theorem

(s : Multiset α) : s = 0 ∨ ∃ a, a ∈ s

Full source

theorem empty_or_exists_mem (s : Multiset α) : s = 0 ∨ ∃ a, a ∈ s :=
  or_iff_not_imp_left.mpr Multiset.exists_mem_of_ne_zero

Empty Multiset or Existence of Member Element

Informal description

For any multiset $s$ over a type $\alpha$, either $s$ is the empty multiset ($s = 0$) or there exists an element $a \in \alpha$ that belongs to $s$.

Multiset.zero_ne_cons theorem

{a : α} {m : Multiset α} : 0 ≠ a ::ₘ m

Full source

@[simp]
theorem zero_ne_cons {a : α} {m : Multiset α} : 0 ≠ a ::ₘ m := fun h =>
  have : a ∈ (0 : Multiset α) := h.symm ▸ mem_cons_self _ _
  not_mem_zero _ this

Non-Equality of Empty Multiset and Insertion: $0 \neq a ::ₘ m$

Informal description

For any element $a$ of type $\alpha$ and any multiset $m$ over $\alpha$, the empty multiset $0$ is not equal to the multiset obtained by adding one occurrence of $a$ to $m$, i.e., $0 \neq a ::ₘ m$.

Multiset.cons_ne_zero theorem

{a : α} {m : Multiset α} : a ::ₘ m ≠ 0

Full source

@[simp]
theorem cons_ne_zero {a : α} {m : Multiset α} : a ::ₘ ma ::ₘ m ≠ 0 :=
  zero_ne_cons.symm

Non-Emptiness of Multiset Insertion: $a ::ₘ m \neq 0$

Informal description

For any element $a$ of type $\alpha$ and any multiset $m$ over $\alpha$, the multiset obtained by adding one occurrence of $a$ to $m$ is not equal to the empty multiset, i.e., $a ::ₘ m \neq 0$.

Multiset.cons_eq_cons theorem

 {a b : α} {as bs : Multiset α} : a ::ₘ as = b ::ₘ bs ↔ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs

Full source

theorem cons_eq_cons {a b : α} {as bs : Multiset α} :
    a ::ₘ asa ::ₘ as = b ::ₘ bs ↔ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs := by
  haveI : DecidableEq α := Classical.decEq α
  constructor
  · intro eq
    by_cases h : a = b
    · subst h
      simp_all
    · have : a ∈ b ::ₘ bs := eq ▸ mem_cons_self _ _
      have : a ∈ bs := by simpa [h]
      rcases exists_cons_of_mem this with ⟨cs, hcs⟩
      simp only [h, hcs, false_and, ne_eq, not_false_eq_true, cons_inj_right, exists_eq_right',
        true_and, false_or]
      have : a ::ₘ as = b ::ₘ a ::ₘ cs := by simp [eq, hcs]
      have : a ::ₘ as = a ::ₘ b ::ₘ cs := by rwa [cons_swap]
      simpa using this
  · intro h
    rcases h with (⟨eq₁, eq₂⟩ | ⟨_, cs, eq₁, eq₂⟩)
    · simp [*]
    · simp [*, cons_swap a b]

Equality Condition for Multiset Insertion: $a ::ₘ as = b ::ₘ bs$ iff $a = b \land as = bs$ or $a \neq b$ with matching tails

Informal description

For any elements $a, b$ of type $\alpha$ and any multisets $as, bs$ over $\alpha$, the equality $a ::ₘ as = b ::ₘ bs$ holds if and only if either: 1. $a = b$ and $as = bs$, or 2. $a \neq b$ and there exists a multiset $cs$ such that $as = b ::ₘ cs$ and $bs = a ::ₘ cs$.

Multiset.instSingleton instance

: Singleton α (Multiset α)

Full source

instance : Singleton α (Multiset α) :=
  ⟨fun a => a ::ₘ 0⟩

Singleton Multiset Construction

Informal description

For any type $\alpha$, there is a singleton operation that constructs a multiset containing exactly one occurrence of a given element $a \in \alpha$.

Multiset.instLawfulSingleton instance

: LawfulSingleton α (Multiset α)

Full source

instance : LawfulSingleton α (Multiset α) :=
  ⟨fun _ => rfl⟩

Lawful Singleton Structure for Multisets

Informal description

For any type $\alpha$, the singleton operation on multisets satisfies the properties of a lawful singleton structure. This means that constructing a singleton multiset $\{a\}$ from an element $a \in \alpha$ behaves as expected with respect to the multiset operations.

Multiset.cons_zero theorem

(a : α) : a ::ₘ 0 = { a }

Full source

@[simp]
theorem cons_zero (a : α) : a ::ₘ 0 = {a} :=
  rfl

Insertion into Empty Multiset Yields Singleton

Informal description

For any element $a$ of type $\alpha$, the multiset obtained by inserting $a$ into the empty multiset is equal to the singleton multiset containing $a$, i.e., $a ::ₘ 0 = \{a\}$.

Multiset.coe_singleton theorem

(a : α) : ([a] : Multiset α) = { a }

Full source

@[simp, norm_cast]
theorem coe_singleton (a : α) : ([a] : Multiset α) = {a} :=
  rfl

Coercion of Singleton List to Singleton Multiset

Informal description

For any element $a$ of type $\alpha$, the multiset obtained by coercing the singleton list $[a]$ is equal to the singleton multiset $\{a\}$, i.e., $[a] = \{a\}$.

Multiset.mem_singleton theorem

{a b : α} : b ∈ ({ a } : Multiset α) ↔ b = a

Full source

@[simp]
theorem mem_singleton {a b : α} : b ∈ ({a} : Multiset α)b ∈ ({a} : Multiset α) ↔ b = a := by
  simp only [← cons_zero, mem_cons, iff_self, or_false, not_mem_zero]

Membership in Singleton Multiset: $b \in \{a\} \leftrightarrow b = a$

Informal description

For any elements $a$ and $b$ of type $\alpha$, the element $b$ belongs to the singleton multiset $\{a\}$ if and only if $b = a$.

Multiset.mem_singleton_self theorem

(a : α) : a ∈ ({ a } : Multiset α)

Full source

theorem mem_singleton_self (a : α) : a ∈ ({a} : Multiset α) := by
  rw [← cons_zero]
  exact mem_cons_self _ _

Self-Membership in Singleton Multiset: $a \in \{a\}$

Informal description

For any element $a$ of type $\alpha$, the element $a$ belongs to the singleton multiset $\{a\}$.

Multiset.singleton_inj theorem

{a b : α} : ({ a } : Multiset α) = { b } ↔ a = b

Full source

@[simp]
theorem singleton_inj {a b : α} : ({a} : Multiset α) = {b} ↔ a = b := by
  simp_rw [← cons_zero]
  exact cons_inj_left _

Equality of Singleton Multisets: $\{a\} = \{b\} \leftrightarrow a = b$

Informal description

For any elements $a$ and $b$ of type $\alpha$, the singleton multisets $\{a\}$ and $\{b\}$ are equal if and only if $a = b$.

Multiset.coe_eq_singleton theorem

{l : List α} {a : α} : (l : Multiset α) = { a } ↔ l = [a]

Full source

@[simp, norm_cast]
theorem coe_eq_singleton {l : List α} {a : α} : (l : Multiset α) = {a} ↔ l = [a] := by
  rw [← coe_singleton, coe_eq_coe, List.perm_singleton]

List-to-Multiset Coercion is Singleton iff List is Singleton: $l = \{a\} \leftrightarrow l = [a]$

Informal description

For any list $l$ of elements of type $\alpha$ and any element $a \in \alpha$, the multiset obtained by coercing $l$ is equal to the singleton multiset $\{a\}$ if and only if $l$ is the singleton list $[a]$. In other words, $l = \{a\}$ as multisets if and only if $l = [a]$ as lists.

Multiset.singleton_eq_cons_iff theorem

{a b : α} (m : Multiset α) : { a } = b ::ₘ m ↔ a = b ∧ m = 0

Full source

@[simp]
theorem singleton_eq_cons_iff {a b : α} (m : Multiset α) : {a}{a} = b ::ₘ m ↔ a = b ∧ m = 0 := by
  rw [← cons_zero, cons_eq_cons]
  simp [eq_comm]

Singleton Multiset Equals Insertion iff Element Matches and Tail is Empty

Informal description

For any elements $a, b$ of type $\alpha$ and any multiset $m$ over $\alpha$, the singleton multiset $\{a\}$ is equal to the multiset $b ::ₘ m$ (obtained by inserting $b$ into $m$) if and only if $a = b$ and $m$ is the empty multiset.

Multiset.pair_comm theorem

(x y : α) : ({ x, y } : Multiset α) = { y, x }

Full source

theorem pair_comm (x y : α) : ({x, y} : Multiset α) = {y, x} :=
  cons_swap x y 0

Commutativity of Multiset Pair Construction: $\{x, y\} = \{y, x\}$

Informal description

For any elements $x$ and $y$ of type $\alpha$, the multiset $\{x, y\}$ is equal to the multiset $\{y, x\}$.

Multiset.zero_subset theorem

(s : Multiset α) : 0 ⊆ s

Full source

@[simp]
theorem zero_subset (s : Multiset α) : 0 ⊆ s := fun _ => not_mem_nil.elim

Empty Multiset is Subset of Any Multiset

Informal description

For any multiset $s$ over a type $\alpha$, the empty multiset $0$ is a subset of $s$.

Multiset.subset_cons theorem

(s : Multiset α) (a : α) : s ⊆ a ::ₘ s

Full source

theorem subset_cons (s : Multiset α) (a : α) : s ⊆ a ::ₘ s := fun _ => mem_cons_of_mem

Subset Property of Multiset Insertion: $s \subseteq a ::ₘ s$

Informal description

For any multiset $s$ over a type $\alpha$ and any element $a$ of type $\alpha$, the multiset $s$ is a subset of the multiset obtained by adding one occurrence of $a$ to $s$ (denoted $a ::ₘ s$).

Multiset.ssubset_cons theorem

{s : Multiset α} {a : α} (ha : a ∉ s) : s ⊂ a ::ₘ s

Full source

theorem ssubset_cons {s : Multiset α} {a : α} (ha : a ∉ s) : s ⊂ a ::ₘ s :=
  ⟨subset_cons _ _, fun h => ha <| h <| mem_cons_self _ _⟩

Strict Subset Property of Multiset Insertion: $s \subset a ::ₘ s$ when $a \notin s$

Informal description

For any multiset $s$ over a type $\alpha$ and any element $a \in \alpha$ not in $s$, the multiset $s$ is a strict subset of the multiset obtained by adding one occurrence of $a$ to $s$, i.e., $s \subset a ::ₘ s$.

Multiset.cons_subset theorem

{a : α} {s t : Multiset α} : a ::ₘ s ⊆ t ↔ a ∈ t ∧ s ⊆ t

Full source

@[simp]
theorem cons_subset {a : α} {s t : Multiset α} : a ::ₘ sa ::ₘ s ⊆ ta ::ₘ s ⊆ t ↔ a ∈ t ∧ s ⊆ t := by
  simp [subset_iff, or_imp, forall_and]

Subset Condition for Multiset Insertion: $a ::ₘ s \subseteq t \leftrightarrow a \in t \land s \subseteq t$

Informal description

For any element $a$ of type $\alpha$ and multisets $s, t$ over $\alpha$, the multiset $a ::ₘ s$ is a subset of $t$ if and only if $a$ is an element of $t$ and $s$ is a subset of $t$.

Multiset.cons_subset_cons theorem

{a : α} {s t : Multiset α} : s ⊆ t → a ::ₘ s ⊆ a ::ₘ t

Full source

theorem cons_subset_cons {a : α} {s t : Multiset α} : s ⊆ t → a ::ₘ sa ::ₘ s ⊆ a ::ₘ t :=
  Quotient.inductionOn₂ s t fun _ _ => List.cons_subset_cons _

Subset Preservation under Multiset Insertion: $s \subseteq t \Rightarrow a \text{::ₘ} s \subseteq a \text{::ₘ} t$

Informal description

For any element $a$ of type $\alpha$ and multisets $s$ and $t$ over $\alpha$, if $s$ is a subset of $t$, then the multiset obtained by adding one occurrence of $a$ to $s$ is a subset of the multiset obtained by adding one occurrence of $a$ to $t$. In other words, if $s \subseteq t$, then $a \text{::ₘ} s \subseteq a \text{::ₘ} t$.

Multiset.subset_zero theorem

: s ⊆ 0 ↔ s = 0

Full source

@[simp] lemma subset_zero : s ⊆ 0s ⊆ 0 ↔ s = 0 :=
  ⟨eq_zero_of_subset_zero, fun xeq => xeq.symm ▸ Subset.refl 0⟩

Subset of Empty Multiset is Empty: $s \subseteq 0 \leftrightarrow s = 0$

Informal description

For any multiset $s$, $s$ is a subset of the empty multiset $0$ if and only if $s$ is equal to $0$.

Multiset.zero_ssubset theorem

: 0 ⊂ s ↔ s ≠ 0

Full source

@[simp] lemma zero_ssubset : 0 ⊂ s0 ⊂ s ↔ s ≠ 0 := by simp [ssubset_iff_subset_not_subset]

Empty Multiset is Strict Subset if and only if Nonempty

Informal description

The empty multiset $0$ is a strict subset of a multiset $s$ if and only if $s$ is not equal to $0$.

Multiset.singleton_subset theorem

: { a } ⊆ s ↔ a ∈ s

Full source

@[simp] lemma singleton_subset : {a}{a} ⊆ s{a} ⊆ s ↔ a ∈ s := by simp [subset_iff]

Singleton Subset Equivalence: $\{a\} \subseteq s \leftrightarrow a \in s$

Informal description

For any element $a$ and multiset $s$, the singleton multiset $\{a\}$ is a subset of $s$ if and only if $a$ is an element of $s$.

Multiset.induction_on' theorem

 {p : Multiset α → Prop} (S : Multiset α) (h₁ : p 0) (h₂ : ∀ {a s}, a ∈ S → s ⊆ S → p s → p (insert a s)) : p S

Full source

theorem induction_on' {p : Multiset α → Prop} (S : Multiset α) (h₁ : p 0)
    (h₂ : ∀ {a s}, a ∈ S → s ⊆ S → p s → p (insert a s)) : p S :=
  @Multiset.induction_on α (fun T => T ⊆ S → p T) S (fun _ => h₁)
    (fun _ _ hps hs =>
      let ⟨hS, sS⟩ := cons_subset.1 hs
      h₂ hS sS (hps sS))
    (Subset.refl S)

Induction Principle for Multisets with Insertion Condition

Informal description

For any predicate $p$ on multisets over a type $\alpha$ and any multiset $S$, if $p$ holds for the empty multiset $0$, and for any element $a \in S$ and multiset $s \subseteq S$, $p(s)$ implies $p(\text{insert}(a, s))$, then $p$ holds for $S$.

Multiset.zero_le theorem

(s : Multiset α) : 0 ≤ s

Full source

theorem zero_le (s : Multiset α) : 0 ≤ s :=
  Quot.inductionOn s fun l => (nil_sublist l).subperm

Empty Multiset is Least Element in Partial Order

Informal description

For any multiset $s$ over a type $\alpha$, the empty multiset $0$ is less than or equal to $s$ in the partial order of multisets.

Multiset.instOrderBot instance

: OrderBot (Multiset α)

Full source

instance : OrderBot (Multiset α) where
  bot := 0
  bot_le := zero_le

Multisets Form an Order with Empty Multiset as Bottom Element

Informal description

The multiset over any type $\alpha$ forms an order with a bottom element, where the empty multiset $0$ is the least element.

Multiset.bot_eq_zero theorem

: (⊥ : Multiset α) = 0

Full source

/-- This is a `rfl` and `simp` version of `bot_eq_zero`. -/
@[simp]
theorem bot_eq_zero : (⊥ : Multiset α) = 0 :=
  rfl

Bottom Element Equals Empty Multiset: $\bot = 0$

Informal description

The bottom element in the partial order of multisets over a type $\alpha$ is equal to the empty multiset $0$.

Multiset.le_zero theorem

: s ≤ 0 ↔ s = 0

Full source

theorem le_zero : s ≤ 0 ↔ s = 0 :=
  le_bot_iff

Characterization of Empty Multiset: $s \leq 0 \leftrightarrow s = 0$

Informal description

For any multiset $s$ over a type $\alpha$, the relation $s \leq 0$ holds if and only if $s$ is the empty multiset $0$.

Multiset.lt_cons_self theorem

(s : Multiset α) (a : α) : s < a ::ₘ s

Full source

theorem lt_cons_self (s : Multiset α) (a : α) : s < a ::ₘ s :=
  Quot.inductionOn s fun l =>
    suffices l <+~ a :: ll <+~ a :: l ∧ ¬l ~ a :: l by simpa [lt_iff_le_and_ne]
    ⟨(sublist_cons_self _ _).subperm,
      fun p => _root_.ne_of_lt (lt_succ_self (length l)) p.length_eq⟩

Strict Submultiset Property: $s < a \cons s$

Informal description

For any multiset $s$ over a type $\alpha$ and any element $a \in \alpha$, the multiset $s$ is strictly contained in the multiset obtained by adding one occurrence of $a$ to $s$, i.e., $s < a \cons s$.

Multiset.le_cons_self theorem

(s : Multiset α) (a : α) : s ≤ a ::ₘ s

Full source

theorem le_cons_self (s : Multiset α) (a : α) : s ≤ a ::ₘ s :=
  le_of_lt <| lt_cons_self _ _

Submultiset Property: $s \leq a \cons s$

Informal description

For any multiset $s$ over a type $\alpha$ and any element $a \in \alpha$, the multiset $s$ is contained in the multiset obtained by adding one occurrence of $a$ to $s$, i.e., $s \leq a \cons s$.

Multiset.cons_le_cons_iff theorem

(a : α) : a ::ₘ s ≤ a ::ₘ t ↔ s ≤ t

Full source

theorem cons_le_cons_iff (a : α) : a ::ₘ sa ::ₘ s ≤ a ::ₘ t ↔ s ≤ t :=
  Quotient.inductionOn₂ s t fun _ _ => subperm_cons a

Multiset Ordering Under Insertion: $a ::ₘ s \leq a ::ₘ t \leftrightarrow s \leq t$

Informal description

For any element $a$ of type $\alpha$ and multisets $s, t$ over $\alpha$, the multiset $a ::ₘ s$ is less than or equal to $a ::ₘ t$ if and only if $s$ is less than or equal to $t$.

Multiset.cons_le_cons theorem

(a : α) : s ≤ t → a ::ₘ s ≤ a ::ₘ t

Full source

theorem cons_le_cons (a : α) : s ≤ t → a ::ₘ s ≤ a ::ₘ t :=
  (cons_le_cons_iff a).2

Multiset Ordering Preserved Under Insertion: $s \leq t \to a \cons s \leq a \cons t$

Informal description

For any element $a$ of type $\alpha$ and multisets $s, t$ over $\alpha$, if $s$ is a submultiset of $t$ (i.e., $s \leq t$), then the multiset obtained by adding one occurrence of $a$ to $s$ is a submultiset of the multiset obtained by adding one occurrence of $a$ to $t$ (i.e., $a \cons s \leq a \cons t$).

Multiset.cons_lt_cons_iff theorem

: a ::ₘ s < a ::ₘ t ↔ s < t

Full source

@[simp] lemma cons_lt_cons_iff : a ::ₘ sa ::ₘ s < a ::ₘ t ↔ s < t :=
  lt_iff_lt_of_le_iff_le' (cons_le_cons_iff _) (cons_le_cons_iff _)

Strict Multiset Ordering Under Insertion: $a ::ₘ s < a ::ₘ t \leftrightarrow s < t$

Informal description

For any element $a$ of type $\alpha$ and multisets $s, t$ over $\alpha$, the multiset $a ::ₘ s$ is strictly less than $a ::ₘ t$ if and only if $s$ is strictly less than $t$.

Multiset.cons_lt_cons theorem

(a : α) (h : s < t) : a ::ₘ s < a ::ₘ t

Full source

lemma cons_lt_cons (a : α) (h : s < t) : a ::ₘ s < a ::ₘ t := cons_lt_cons_iff.2 h

Strict Multiset Ordering Preserved Under Insertion: $s < t \to a ::ₘ s < a ::ₘ t$

Informal description

For any element $a$ of type $\alpha$ and multisets $s, t$ over $\alpha$, if $s$ is strictly less than $t$ (i.e., $s < t$), then the multiset obtained by adding one occurrence of $a$ to $s$ is strictly less than the multiset obtained by adding one occurrence of $a$ to $t$ (i.e., $a ::ₘ s < a ::ₘ t$).

Multiset.le_cons_of_not_mem theorem

(m : a ∉ s) : s ≤ a ::ₘ t ↔ s ≤ t

Full source

theorem le_cons_of_not_mem (m : a ∉ s) : s ≤ a ::ₘ t ↔ s ≤ t := by
  refine ⟨?_, fun h => le_trans h <| le_cons_self _ _⟩
  suffices ∀ {t'}, s ≤ t' → a ∈ t' → a ::ₘ s ≤ t' by
    exact fun h => (cons_le_cons_iff a).1 (this h (mem_cons_self _ _))
  introv h
  revert m
  refine leInductionOn h ?_
  introv s m₁ m₂
  rcases append_of_mem m₂ with ⟨r₁, r₂, rfl⟩
  exact
    perm_middle.subperm_left.2
      ((subperm_cons _).2 <| ((sublist_or_mem_of_sublist s).resolve_right m₁).subperm)

Submultiset Condition Under Insertion of Non-Member Element: $s \leq a ::ₘ t \leftrightarrow s \leq t$ when $a \notin s$

Informal description

For any element $a$ of type $\alpha$ and multisets $s, t$ over $\alpha$, if $a$ is not in $s$, then $s$ is a submultiset of $a ::ₘ t$ if and only if $s$ is a submultiset of $t$.

Multiset.cons_le_of_not_mem theorem

(hs : a ∉ s) : a ::ₘ s ≤ t ↔ a ∈ t ∧ s ≤ t

Full source

theorem cons_le_of_not_mem (hs : a ∉ s) : a ::ₘ sa ::ₘ s ≤ t ↔ a ∈ t ∧ s ≤ t := by
  apply Iff.intro (fun h ↦ ⟨subset_of_le h (mem_cons_self a s), le_trans (le_cons_self s a) h⟩)
  rintro ⟨h₁, h₂⟩; rcases exists_cons_of_mem h₁ with ⟨_, rfl⟩
  exact cons_le_cons _ ((le_cons_of_not_mem hs).mp h₂)

Submultiset Condition for Inserted Element: $a ::ₘ s \leq t \leftrightarrow (a \in t \land s \leq t)$ when $a \notin s$

Informal description

For any element $a$ of type $\alpha$ and multisets $s, t$ over $\alpha$, if $a$ is not in $s$, then the multiset $a ::ₘ s$ is a submultiset of $t$ if and only if $a$ is in $t$ and $s$ is a submultiset of $t$.

Multiset.singleton_ne_zero theorem

(a : α) : ({ a } : Multiset α) ≠ 0

Full source

@[simp]
theorem singleton_ne_zero (a : α) : ({a} : Multiset α) ≠ 0 :=
  ne_of_gt (lt_cons_self _ _)

Non-emptiness of Singleton Multiset: $\{a\} \neq 0$

Informal description

For any element $a$ of type $\alpha$, the singleton multiset $\{a\}$ is not equal to the empty multiset $0$.

Multiset.zero_ne_singleton theorem

(a : α) : 0 ≠ ({ a } : Multiset α)

Full source

@[simp]
theorem zero_ne_singleton (a : α) : 0 ≠ ({a} : Multiset α) := singleton_ne_zero _ |>.symm

Non-equality of Empty and Singleton Multisets: $0 \neq \{a\}$

Informal description

For any element $a$ of type $\alpha$, the empty multiset $0$ is not equal to the singleton multiset $\{a\}$.

Multiset.singleton_le theorem

{a : α} {s : Multiset α} : { a } ≤ s ↔ a ∈ s

Full source

@[simp]
theorem singleton_le {a : α} {s : Multiset α} : {a}{a} ≤ s ↔ a ∈ s :=
  ⟨fun h => mem_of_le h (mem_singleton_self _), fun h =>
    let ⟨_t, e⟩ := exists_cons_of_mem h
    e.symm ▸ cons_le_cons _ (zero_le _)⟩

Singleton Submultiset Condition: $\{a\} \leq s \leftrightarrow a \in s$

Informal description

For any element $a$ of type $\alpha$ and any multiset $s$ over $\alpha$, the singleton multiset $\{a\}$ is a submultiset of $s$ if and only if $a$ is an element of $s$.

Multiset.le_singleton theorem

: s ≤ { a } ↔ s = 0 ∨ s = { a }

Full source

@[simp] lemma le_singleton : s ≤ {a} ↔ s = 0 ∨ s = {a} :=
  Quot.induction_on s fun l ↦ by simp only [cons_zero, ← coe_singleton, quot_mk_to_coe'', coe_le,
    coe_eq_zero, coe_eq_coe, perm_singleton, subperm_singleton_iff]

Characterization of Multiset Ordering with Singleton: $s \leq \{a\} \leftrightarrow s = 0 \lor s = \{a\}$

Informal description

For any multiset $s$ and element $a$ of type $\alpha$, the multiset $s$ is less than or equal to the singleton multiset $\{a\}$ if and only if $s$ is the empty multiset $0$ or $s$ is equal to $\{a\}$ itself.

Multiset.lt_singleton theorem

: s < { a } ↔ s = 0

Full source

@[simp] lemma lt_singleton : s < {a} ↔ s = 0 := by
  simp only [lt_iff_le_and_ne, le_singleton, or_and_right, Ne, and_not_self, or_false,
    and_iff_left_iff_imp]
  rintro rfl
  exact (singleton_ne_zero _).symm

Characterization of Strict Multiset Ordering with Singleton: $s < \{a\} \leftrightarrow s = 0$

Informal description

For any multiset $s$ and element $a$ of type $\alpha$, the multiset $s$ is strictly less than the singleton multiset $\{a\}$ if and only if $s$ is the empty multiset $0$.

Multiset.ssubset_singleton_iff theorem

: s ⊂ { a } ↔ s = 0

Full source

@[simp] lemma ssubset_singleton_iff : s ⊂ {a}s ⊂ {a} ↔ s = 0 := by
  refine ⟨fun hs ↦ eq_zero_of_subset_zero fun b hb ↦ (hs.2 ?_).elim, ?_⟩
  · obtain rfl := mem_singleton.1 (hs.1 hb)
    rwa [singleton_subset]
  · rintro rfl
    simp

Characterization of Strict Subset Relation with Singleton Multiset: $s \subset \{a\} \leftrightarrow s = 0$

Informal description

For any multiset $s$ and element $a$ of type $\alpha$, the multiset $s$ is a strict subset of the singleton multiset $\{a\}$ if and only if $s$ is the empty multiset $0$.

Multiset.card_zero theorem

: @card α 0 = 0

Full source

@[simp]
theorem card_zero : @card α 0 = 0 :=
  rfl

Cardinality of Empty Multiset: $|0| = 0$

Informal description

The cardinality of the empty multiset over a type $\alpha$ is $0$, i.e., $|0| = 0$.

Multiset.card_cons theorem

(a : α) (s : Multiset α) : card (a ::ₘ s) = card s + 1

Full source

@[simp]
theorem card_cons (a : α) (s : Multiset α) : card (a ::ₘ s) = card s + 1 :=
  Quot.inductionOn s fun _l => rfl

Cardinality of Multiset Insertion: $|a ::ₘ s| = |s| + 1$

Informal description

For any element $a$ of type $\alpha$ and any multiset $s$ over $\alpha$, the cardinality of the multiset obtained by inserting $a$ into $s$ (denoted $a ::ₘ s$) is equal to the cardinality of $s$ plus one, i.e., $|a ::ₘ s| = |s| + 1$.

Multiset.card_singleton theorem

(a : α) : card ({ a } : Multiset α) = 1

Full source

@[simp]
theorem card_singleton (a : α) : card ({a} : Multiset α) = 1 := by
  simp only [← cons_zero, card_zero, eq_self_iff_true, card_cons]

Cardinality of Singleton Multiset: $|\{a\}| = 1$

Informal description

For any element $a$ of type $\alpha$, the cardinality of the singleton multiset $\{a\}$ is equal to 1, i.e., $|\{a\}| = 1$.

Multiset.card_pair theorem

(a b : α) : card { a, b } = 2

Full source

theorem card_pair (a b : α) : card {a, b} = 2 := by
  rw [insert_eq_cons, card_cons, card_singleton]

Cardinality of Pair Multiset: $|\{a, b\}| = 2$

Informal description

For any two elements $a$ and $b$ of type $\alpha$, the cardinality of the multiset $\{a, b\}$ is equal to 2, i.e., $|\{a, b\}| = 2$.

Multiset.card_eq_one theorem

{s : Multiset α} : card s = 1 ↔ ∃ a, s = { a }

Full source

theorem card_eq_one {s : Multiset α} : cardcard s = 1 ↔ ∃ a, s = {a} :=
  ⟨Quot.inductionOn s fun _l h => (List.length_eq_one_iff.1 h).imp fun _a => congr_arg _,
    fun ⟨_a, e⟩ => e.symm ▸ rfl⟩

Cardinality One Characterization for Multisets: $|s| = 1 \leftrightarrow \exists a, s = \{a\}$

Informal description

For any multiset $s$ over a type $\alpha$, the cardinality of $s$ is equal to 1 if and only if there exists an element $a \in \alpha$ such that $s$ is the singleton multiset $\{a\}$.

Multiset.lt_iff_cons_le theorem

{s t : Multiset α} : s < t ↔ ∃ a, a ::ₘ s ≤ t

Full source

theorem lt_iff_cons_le {s t : Multiset α} : s < t ↔ ∃ a, a ::ₘ s ≤ t :=
  ⟨Quotient.inductionOn₂ s t fun _l₁ _l₂ h =>
      Subperm.exists_of_length_lt (le_of_lt h) (card_lt_card h),
    fun ⟨_a, h⟩ => lt_of_lt_of_le (lt_cons_self _ _) h⟩

Characterization of Strict Submultiset via Insertion and Order

Informal description

For any multisets $s$ and $t$ over a type $\alpha$, $s$ is strictly contained in $t$ if and only if there exists an element $a \in \alpha$ such that the multiset obtained by adding one occurrence of $a$ to $s$ is less than or equal to $t$, i.e., $s < t \leftrightarrow \exists a, a \cons s \leq t$.

Multiset.card_eq_zero theorem

{s : Multiset α} : card s = 0 ↔ s = 0

Full source

@[simp]
theorem card_eq_zero {s : Multiset α} : cardcard s = 0 ↔ s = 0 :=
  ⟨fun h => (eq_of_le_of_card_le (zero_le _) (le_of_eq h)).symm, fun e => by simp [e]⟩

Zero Cardinality Characterization for Multisets: $|s| = 0 \leftrightarrow s = 0$

Informal description

For any multiset $s$ over a type $\alpha$, the cardinality of $s$ is zero if and only if $s$ is the empty multiset, i.e., $|s| = 0 \leftrightarrow s = 0$.

Multiset.card_pos theorem

{s : Multiset α} : 0 < card s ↔ s ≠ 0

Full source

theorem card_pos {s : Multiset α} : 0 < card s ↔ s ≠ 0 :=
  Nat.pos_iff_ne_zero.trans <| not_congr card_eq_zero

Positive Cardinality Characterization for Multisets: $|s| > 0 \leftrightarrow s \neq 0$

Informal description

For any multiset $s$ over a type $\alpha$, the cardinality of $s$ is positive if and only if $s$ is not the empty multiset, i.e., $|s| > 0 \leftrightarrow s \neq 0$.

Multiset.card_pos_iff_exists_mem theorem

{s : Multiset α} : 0 < card s ↔ ∃ a, a ∈ s

Full source

theorem card_pos_iff_exists_mem {s : Multiset α} : 0 < card s ↔ ∃ a, a ∈ s :=
  Quot.inductionOn s fun _l => length_pos_iff_exists_mem

Positive Cardinality of Multiset Equivalent to Non-Emptiness

Informal description

For any multiset $s$ over a type $\alpha$, the cardinality of $s$ is positive if and only if there exists an element $a \in \alpha$ that belongs to $s$. In other words, $|s| > 0 \leftrightarrow \exists a, a \in s$.

Multiset.card_eq_two theorem

{s : Multiset α} : card s = 2 ↔ ∃ x y, s = { x, y }

Full source

theorem card_eq_two {s : Multiset α} : cardcard s = 2 ↔ ∃ x y, s = {x, y} :=
  ⟨Quot.inductionOn s fun _l h =>
      (List.length_eq_two.mp h).imp fun _a => Exists.imp fun _b => congr_arg _,
    fun ⟨_a, _b, e⟩ => e.symm ▸ rfl⟩

Multiset Cardinality Equals Two if and only if It's a Pair $\{x, y\}$

Informal description

For any multiset $s$ over a type $\alpha$, the cardinality of $s$ is equal to 2 if and only if there exist elements $x, y \in \alpha$ such that $s$ is the multiset $\{x, y\}$ (containing exactly one occurrence of $x$ and one occurrence of $y$).

Multiset.card_eq_three theorem

{s : Multiset α} : card s = 3 ↔ ∃ x y z, s = { x, y, z }

Full source

theorem card_eq_three {s : Multiset α} : cardcard s = 3 ↔ ∃ x y z, s = {x, y, z} :=
  ⟨Quot.inductionOn s fun _l h =>
      (List.length_eq_three.mp h).imp fun _a =>
        Exists.imp fun _b => Exists.imp fun _c => congr_arg _,
    fun ⟨_a, _b, _c, e⟩ => e.symm ▸ rfl⟩

Multiset Cardinality Equals Three if and only if It's a Triple $\{x, y, z\}$

Informal description

For any multiset $s$ over a type $\alpha$, the cardinality of $s$ is equal to 3 if and only if there exist elements $x, y, z \in \alpha$ such that $s$ is the multiset $\{x, y, z\}$ (containing exactly one occurrence of each of $x$, $y$, and $z$).

Multiset.pmap_zero theorem

{p : α → Prop} (f : ∀ a, p a → β) (h : ∀ a ∈ (0 : Multiset α), p a) : pmap f 0 h = 0

Full source

@[simp]
theorem pmap_zero {p : α → Prop} (f : ∀ a, p a → β) (h : ∀ a ∈ (0 : Multiset α), p a) :
    pmap f 0 h = 0 :=
  rfl

Partial Map of Empty Multiset is Empty

Informal description

For any predicate $p$ on elements of type $\alpha$ and any function $f$ that maps elements satisfying $p$ to type $\beta$, if $h$ is a proof that all elements in the empty multiset $0$ satisfy $p$, then the partial map `pmap f 0 h` is equal to the empty multiset $0$.

Multiset.pmap_cons theorem

 {p : α → Prop} (f : ∀ a, p a → β) (a : α) (m : Multiset α) :
  ∀ h : ∀ b ∈ a ::ₘ m, p b,
    pmap f (a ::ₘ m) h = f a (h a (mem_cons_self a m)) ::ₘ pmap f m fun a ha => h a <| mem_cons_of_mem ha

Full source

@[simp]
theorem pmap_cons {p : α → Prop} (f : ∀ a, p a → β) (a : α) (m : Multiset α) :
    ∀ h : ∀ b ∈ a ::ₘ m, p b,
      pmap f (a ::ₘ m) h =
        f a (h a (mem_cons_self a m)) ::ₘ pmap f m fun a ha => h a <| mem_cons_of_mem ha :=
  Quotient.inductionOn m fun _l _h => rfl

Partial Map of Cons Multiset: $\text{pmap}\, f\, (a ::ₘ m)\, h = f a (h a (a \in a ::ₘ m)) ::ₘ \text{pmap}\, f\, m\, (\lambda a\, ha, h a (ha \Rightarrow a \in a ::ₘ m))$

Informal description

For any predicate $p$ on elements of type $\alpha$, any function $f \colon \forall a, p(a) \to \beta$, any element $a \in \alpha$, and any multiset $m$ over $\alpha$, given a proof $h$ that all elements in $a ::ₘ m$ satisfy $p$, the partial map $\text{pmap}\, f\, (a ::ₘ m)\, h$ is equal to the multiset obtained by applying $f$ to $a$ (with proof $h a (a \in a ::ₘ m)$) and then adding this to the partial map of $m$ under $f$ (with proof that all elements of $m$ satisfy $p$ via $h$).

Multiset.attach_zero theorem

: (0 : Multiset α).attach = 0

Full source

@[simp]
theorem attach_zero : (0 : Multiset α).attach = 0 :=
  rfl

Attachment of Empty Multiset is Empty

Informal description

The attachment of the empty multiset $0$ is equal to the empty multiset itself, i.e., $(0 : \text{Multiset } \alpha).\text{attach} = 0$.

Multiset.Rel inductive

(r : α → β → Prop) : Multiset α → Multiset β → Prop

Full source

/-- `Rel r s t` -- lift the relation `r` between two elements to a relation between `s` and `t`,
s.t. there is a one-to-one mapping between elements in `s` and `t` following `r`. -/
@[mk_iff]
inductive Rel (r : α → β → Prop) : Multiset α → Multiset β → Prop
  | zero : Rel r 0 0
  | cons {a b as bs} : r a b → Rel r as bs → Rel r (a ::ₘ as) (b ::ₘ bs)

Lifting a relation to multisets

Informal description

The relation `Rel r s t` between multisets `s` and `t` lifts a binary relation `r` between elements of `α` and `β` to a relation between multisets over `α` and `β`. Specifically, `Rel r s t` holds if there exists a one-to-one correspondence between the elements of `s` and `t` such that for every pair of corresponding elements `a ∈ s` and `b ∈ t`, the relation `r a b` holds.

Multiset.rel_flip theorem

{s t} : Rel (flip r) s t ↔ Rel r t s

Full source

theorem rel_flip {s t} : RelRel (flip r) s t ↔ Rel r t s :=
  ⟨rel_flip_aux, rel_flip_aux⟩

Flip of Lifted Relation on Multisets is Equivalent to Reverse Lifting

Informal description

For any relation $r : \alpha \to \beta \to \text{Prop}$ and multisets $s$ and $t$, the relation $\text{Rel}(\text{flip}\, r)\, s\, t$ holds if and only if $\text{Rel}\, r\, t\, s$ holds. Here, $\text{flip}\, r$ denotes the relation obtained by reversing the arguments of $r$, i.e., $(\text{flip}\, r)\, b\, a = r\, a\, b$.

Multiset.rel_refl_of_refl_on theorem

{m : Multiset α} {r : α → α → Prop} : (∀ x ∈ m, r x x) → Rel r m m

Full source

theorem rel_refl_of_refl_on {m : Multiset α} {r : α → α → Prop} : (∀ x ∈ m, r x x) → Rel r m m := by
  refine m.induction_on ?_ ?_
  · intros
    apply Rel.zero
  · intro a m ih h
    exact Rel.cons (h _ (mem_cons_self _ _)) (ih fun _ ha => h _ (mem_cons_of_mem ha))

Reflexivity of Lifted Relation on Multisets

Informal description

For any multiset $m$ over a type $\alpha$ and any reflexive relation $r$ on $\alpha$ (i.e., $r(x, x)$ holds for all $x \in m$), the lifted relation $\text{Rel}\, r\, m\, m$ holds.

Multiset.rel_eq_refl theorem

{s : Multiset α} : Rel (· = ·) s s

Full source

theorem rel_eq_refl {s : Multiset α} : Rel (· = ·) s s :=
  rel_refl_of_refl_on fun _x _hx => rfl

Reflexivity of Lifted Equality Relation on Multisets

Informal description

For any multiset $s$ over a type $\alpha$, the lifted relation $\text{Rel}\, (=)\, s\, s$ holds, where $(=)$ denotes the equality relation on $\alpha$.

Multiset.rel_eq theorem

{s t : Multiset α} : Rel (· = ·) s t ↔ s = t

Full source

theorem rel_eq {s t : Multiset α} : RelRel (· = ·) s t ↔ s = t := by
  constructor
  · intro h
    induction h <;> simp [*]
  · intro h
    subst h
    exact rel_eq_refl

Equivalence of Lifted Equality Relation and Multiset Equality

Informal description

For any two multisets $s$ and $t$ over a type $\alpha$, the lifted equality relation $\text{Rel}\, (=)\, s\, t$ holds if and only if $s = t$.

Multiset.Rel.mono theorem

{r p : α → β → Prop} {s t} (hst : Rel r s t) (h : ∀ a ∈ s, ∀ b ∈ t, r a b → p a b) : Rel p s t

Full source

theorem Rel.mono {r p : α → β → Prop} {s t} (hst : Rel r s t)
    (h : ∀ a ∈ s, ∀ b ∈ t, r a b → p a b) : Rel p s t := by
  induction hst with
  | zero => exact Rel.zero
  | @cons a b s t hab _hst ih =>
    apply Rel.cons (h a (mem_cons_self _ _) b (mem_cons_self _ _) hab)
    exact ih fun a' ha' b' hb' h' => h a' (mem_cons_of_mem ha') b' (mem_cons_of_mem hb') h'

Monotonicity of Lifted Relation on Multisets

Informal description

Let $r$ and $p$ be binary relations between types $\alpha$ and $\beta$, and let $s$ and $t$ be multisets over $\alpha$ and $\beta$ respectively. If $\text{Rel}(r, s, t)$ holds and for every $a \in s$ and $b \in t$, $r(a, b)$ implies $p(a, b)$, then $\text{Rel}(p, s, t)$ holds.

Multiset.rel_flip_eq theorem

{s t : Multiset α} : Rel (fun a b => b = a) s t ↔ s = t

Full source

theorem rel_flip_eq {s t : Multiset α} : RelRel (fun a b => b = a) s t ↔ s = t :=
  show RelRel (flip (· = ·)) s t ↔ s = t by rw [rel_flip, rel_eq, eq_comm]

Equivalence of Flipped Equality Relation and Multiset Equality

Informal description

For any two multisets $s$ and $t$ over a type $\alpha$, the relation $\text{Rel}\,(\lambda a b, b = a)\,s\,t$ holds if and only if $s = t$.

Multiset.rel_zero_left theorem

{b : Multiset β} : Rel r 0 b ↔ b = 0

Full source

@[simp]
theorem rel_zero_left {b : Multiset β} : RelRel r 0 b ↔ b = 0 := by rw [rel_iff]; simp

Empty Multiset Relation: $\text{Rel}\,r\,0\,b \leftrightarrow b = 0$

Informal description

For any multiset $b$ over a type $\beta$ and any relation $r$ between elements of $\alpha$ and $\beta$, the relation $\text{Rel}\,r\,0\,b$ holds if and only if $b$ is the empty multiset $0$.

Multiset.rel_zero_right theorem

{a : Multiset α} : Rel r a 0 ↔ a = 0

Full source

@[simp]
theorem rel_zero_right {a : Multiset α} : RelRel r a 0 ↔ a = 0 := by rw [rel_iff]; simp

Empty Multiset Relation: $\text{Rel}\,r\,a\,0 \leftrightarrow a = 0$

Informal description

For any multiset $a$ over a type $\alpha$ and any relation $r : \alpha \to \beta \to \text{Prop}$, the relation $\text{Rel}\,r\,a\,0$ holds if and only if $a$ is the empty multiset (i.e., $a = 0$).

Multiset.rel_cons_left theorem

{a as bs} : Rel r (a ::ₘ as) bs ↔ ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs'

Full source

theorem rel_cons_left {a as bs} :
    RelRel r (a ::ₘ as) bs ↔ ∃ b bs', r a b ∧ Rel r as bs' ∧ bs = b ::ₘ bs' := by
  constructor
  · generalize hm : a ::ₘ as = m
    intro h
    induction h generalizing as with
    | zero => simp at hm
    | @cons a' b as' bs ha'b h ih =>
      rcases cons_eq_cons.1 hm with (⟨eq₁, eq₂⟩ | ⟨_h, cs, eq₁, eq₂⟩)
      · subst eq₁
        subst eq₂
        exact ⟨b, bs, ha'b, h, rfl⟩
      · rcases ih eq₂.symm with ⟨b', bs', h₁, h₂, eq⟩
        exact ⟨b', b ::ₘ bs', h₁, eq₁.symm ▸ Rel.cons ha'b h₂, eq.symm ▸ cons_swap _ _ _⟩
  · exact fun ⟨b, bs', hab, h, Eq⟩ => Eq.symm ▸ Rel.cons hab h

Lifting Relation to Multiset Insertion: $\text{Rel}\,r\,(a ::ₘ as)\,bs$ iff Matching Head and Tail

Informal description

For any relation $r$ between elements of types $\alpha$ and $\beta$, any element $a \in \alpha$, and any multisets $as$ over $\alpha$ and $bs$ over $\beta$, the relation $\text{Rel}\,r\,(a ::ₘ as)\,bs$ holds if and only if there exist an element $b \in \beta$ and a multiset $bs'$ over $\beta$ such that: 1. $r\,a\,b$ holds, 2. $\text{Rel}\,r\,as\,bs'$ holds, and 3. $bs = b ::ₘ bs'$.

Multiset.rel_cons_right theorem

{as b bs} : Rel r as (b ::ₘ bs) ↔ ∃ a as', r a b ∧ Rel r as' bs ∧ as = a ::ₘ as'

Full source

theorem rel_cons_right {as b bs} :
    RelRel r as (b ::ₘ bs) ↔ ∃ a as', r a b ∧ Rel r as' bs ∧ as = a ::ₘ as' := by
  rw [← rel_flip, rel_cons_left]
  refine exists₂_congr fun a as' => ?_
  rw [rel_flip, flip]

Lifting Relation to Multiset Insertion: $\text{Rel}\,r\,as\,(b ::ₘ bs)$ iff Matching Head and Tail

Informal description

For any relation $r : \alpha \to \beta \to \text{Prop}$, any element $b \in \beta$, and any multisets $as$ over $\alpha$ and $bs$ over $\beta$, the relation $\text{Rel}\,r\,as\,(b ::ₘ bs)$ holds if and only if there exist an element $a \in \alpha$ and a multiset $as'$ over $\alpha$ such that: 1. $r\,a\,b$ holds, 2. $\text{Rel}\,r\,as'\,bs$ holds, and 3. $as = a ::ₘ as'$.

Multiset.card_eq_card_of_rel theorem

{r : α → β → Prop} {s : Multiset α} {t : Multiset β} (h : Rel r s t) : card s = card t

Full source

theorem card_eq_card_of_rel {r : α → β → Prop} {s : Multiset α} {t : Multiset β} (h : Rel r s t) :
    card s = card t := by induction h <;> simp [*]

Cardinality Preservation under Multiset Relation: $|s| = |t|$ when $\text{Rel}\,r\,s\,t$ holds

Informal description

For any relation $r : \alpha \to \beta \to \text{Prop}$ and multisets $s$ over $\alpha$ and $t$ over $\beta$, if $\text{Rel}\,r\,s\,t$ holds, then the cardinality of $s$ is equal to the cardinality of $t$, i.e., $|s| = |t|$.

Multiset.exists_mem_of_rel_of_mem theorem

 {r : α → β → Prop} {s : Multiset α} {t : Multiset β} (h : Rel r s t) : ∀ {a : α}, a ∈ s → ∃ b ∈ t, r a b

Full source

theorem exists_mem_of_rel_of_mem {r : α → β → Prop} {s : Multiset α} {t : Multiset β}
    (h : Rel r s t) : ∀ {a : α}, a ∈ s → ∃ b ∈ t, r a b := by
  induction h with
  | zero => simp
  | @cons x y s t hxy _ ih =>
    intro a ha
    rcases mem_cons.1 ha with ha | ha
    · exact ⟨y, mem_cons_self _ _, ha.symm ▸ hxy⟩
    · rcases ih ha with ⟨b, hbt, hab⟩
      exact ⟨b, mem_cons.2 (Or.inr hbt), hab⟩

Existence of Related Elements in Multiset Relation

Informal description

Let $r : \alpha \to \beta \to \text{Prop}$ be a relation, and let $s$ and $t$ be multisets over $\alpha$ and $\beta$ respectively. If $\text{Rel}\ r\ s\ t$ holds, then for every element $a \in s$, there exists an element $b \in t$ such that $r\ a\ b$ holds.

Multiset.rel_of_forall theorem

 {m1 m2 : Multiset α} {r : α → α → Prop} (h : ∀ a b, a ∈ m1 → b ∈ m2 → r a b) (hc : card m1 = card m2) : m1.Rel r m2

Full source

theorem rel_of_forall {m1 m2 : Multiset α} {r : α → α → Prop} (h : ∀ a b, a ∈ m1 → b ∈ m2 → r a b)
    (hc : card m1 = card m2) : m1.Rel r m2 := by
  revert m1
  refine @(m2.induction_on ?_ ?_)
  · intro m _h hc
    rw [rel_zero_right, ← card_eq_zero, hc, card_zero]
  · intro a t ih m h hc
    rw [card_cons] at hc
    obtain ⟨b, hb⟩ := card_pos_iff_exists_mem.1 (show 0 < card m from hc.symm ▸ Nat.succ_pos _)
    obtain ⟨m', rfl⟩ := exists_cons_of_mem hb
    refine rel_cons_right.mpr ⟨b, m', h _ _ hb (mem_cons_self _ _), ih ?_ ?_, rfl⟩
    · exact fun _ _ ha hb => h _ _ (mem_cons_of_mem ha) (mem_cons_of_mem hb)
    · simpa using hc

Lifting Pairwise Relation to Multisets with Equal Cardinality: $\text{Rel}\,r\,m_1\,m_2$ when $r(a,b)$ for all $a \in m_1, b \in m_2$ and $|m_1| = |m_2|$

Informal description

For any two multisets $m_1$ and $m_2$ over a type $\alpha$ and any relation $r : \alpha \to \alpha \to \text{Prop}$, if for every $a \in m_1$ and $b \in m_2$ the relation $r(a, b)$ holds, and the cardinalities of $m_1$ and $m_2$ are equal, then the lifted relation $\text{Rel}\,r\,m_1\,m_2$ holds between the multisets.

Multiset.Rel.trans theorem

(r : α → α → Prop) [IsTrans α r] {s t u : Multiset α} (r1 : Rel r s t) (r2 : Rel r t u) : Rel r s u

Full source

protected nonrec
theorem Rel.trans (r : α → α → Prop) [IsTrans α r] {s t u : Multiset α} (r1 : Rel r s t)
    (r2 : Rel r t u) : Rel r s u := by
  induction t using Multiset.induction_on generalizing s u with
  | empty => rw [rel_zero_right.mp r1, rel_zero_left.mp r2, rel_zero_left]
  | cons x t ih =>
    obtain ⟨a, as, ha1, ha2, rfl⟩ := rel_cons_right.mp r1
    obtain ⟨b, bs, hb1, hb2, rfl⟩ := rel_cons_left.mp r2
    exact Multiset.Rel.cons (_root_.trans ha1 hb1) (ih ha2 hb2)

Transitivity of Lifted Relation on Multisets

Informal description

Let $r : \alpha \to \alpha \to \text{Prop}$ be a transitive relation on a type $\alpha$. For any multisets $s, t, u$ over $\alpha$, if $\text{Rel}\,r\,s\,t$ and $\text{Rel}\,r\,t\,u$ hold, then $\text{Rel}\,r\,s\,u$ also holds. Here, $\text{Rel}\,r$ denotes the lifting of $r$ to multisets, which requires a one-to-one correspondence between elements preserving $r$.

Multiset.pairwise_zero theorem

(r : α → α → Prop) : Multiset.Pairwise r 0

Full source

@[simp]
theorem pairwise_zero (r : α → α → Prop) : Multiset.Pairwise r 0 :=
  ⟨[], rfl, List.Pairwise.nil⟩

Empty Multiset is Pairwise for Any Relation

Informal description

For any binary relation $r$ on elements of type $\alpha$, the empty multiset $0$ satisfies the pairwise property with respect to $r$.

Multiset.nodup_zero theorem

: @Nodup α 0

Full source

@[simp]
theorem nodup_zero : @Nodup α 0 :=
  Pairwise.nil

Empty Multiset Has No Duplicates

Informal description

The empty multiset $0$ over a type $\alpha$ has no duplicate elements.

Multiset.nodup_cons theorem

{a : α} {s : Multiset α} : Nodup (a ::ₘ s) ↔ a ∉ s ∧ Nodup s

Full source

@[simp]
theorem nodup_cons {a : α} {s : Multiset α} : NodupNodup (a ::ₘ s) ↔ a ∉ s ∧ Nodup s :=
  Quot.induction_on s fun _ => List.nodup_cons

Characterization of No-Duplicates in Multiset Insertion

Informal description

For any element $a$ of type $\alpha$ and any multiset $s$ over $\alpha$, the multiset $a ::ₘ s$ has no duplicate elements if and only if $a$ does not belong to $s$ and $s$ itself has no duplicates.

Multiset.Nodup.cons theorem

(m : a ∉ s) (n : Nodup s) : Nodup (a ::ₘ s)

Full source

theorem Nodup.cons (m : a ∉ s) (n : Nodup s) : Nodup (a ::ₘ s) :=
  nodup_cons.2 ⟨m, n⟩

Preservation of No-Duplicates under Multiset Insertion

Informal description

Given an element $a$ of type $\alpha$ and a multiset $s$ over $\alpha$, if $a$ is not in $s$ and $s$ has no duplicates, then the multiset $a ::ₘ s$ also has no duplicates.

Multiset.Nodup.of_cons theorem

(h : Nodup (a ::ₘ s)) : Nodup s

Full source

theorem Nodup.of_cons (h : Nodup (a ::ₘ s)) : Nodup s :=
  (nodup_cons.1 h).2

No-Duplicates Preservation in Multiset Deconstruction

Informal description

If the multiset obtained by inserting an element $a$ into a multiset $s$ (denoted $a ::ₘ s$) has no duplicates, then the original multiset $s$ also has no duplicates.

Multiset.Nodup.not_mem theorem

(h : Nodup (a ::ₘ s)) : a ∉ s

Full source

theorem Nodup.not_mem (h : Nodup (a ::ₘ s)) : a ∉ s :=
  (nodup_cons.1 h).1

No-Duplicates Implies Non-Membership in Multiset Insertion

Informal description

If the multiset $a ::ₘ s$ has no duplicates, then the element $a$ does not belong to the multiset $s$.

Mathlib.Data.Multiset.ZeroCons

Notation

Main results