def Multiset.atom {α : Type u_1} (a : α) : Multiset α

Function to avoid reducing {a} + s to a ::ₘ s

Equations

• ⦃a⦄ = {a}

def Multiset.«term⦃_⦄» : Lean.ParserDescr

⦃x, y, z, ...⦄ notation for kpair

Equations

• One or more equations did not get rendered due to their size.

def Multiset.pairUnexpander : Lean.PrettyPrinter.Unexpander

Equations

• One or more equations did not get rendered due to their size.

theorem Multiset.atom_eq_singleton {α : Type u_1} (a : α) : ⦃a⦄ = {a}

theorem Multiset.add_atom_eq_cons {α : Type u_1} (a : α) (s : Multiset α) : s + ⦃a⦄ = a ::ₘ s

@[simp]

theorem Multiset.mem_atom_iff {α : Type u_1} {a b : α} : a ∈ ⦃b⦄ ↔ a = b

@[simp]

theorem Multiset.atom_le_iff {α : Type u_1} {a : α} {s : Multiset α} : ⦃a⦄ ≤ s ↔ a ∈ s

@[simp]

theorem Multiset.atom_subset_iff {α : Type u_1} {a : α} {s : Multiset α} : ⦃a⦄ ⊆ s ↔ a ∈ s

@[simp]

theorem Multiset.map_atom {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) : map f ⦃a⦄ = ⦃f a⦄

@[simp]

theorem Multiset.forall_mem_add {α : Type u_1} {p : α → Prop} {s t : Multiset α} : (∀ (a : α), a ∈ s + t → p a) ↔ (∀ (a : α), a ∈ s → p a) ∧ ∀ (a : α), a ∈ t → p a

Universal membership over a sum splits into the two summands. This is a routine property of multiset membership.

@[simp]

theorem Multiset.forall_mem_atom {α : Type u_1} {p : α → Prop} {a : α} : (∀ (b : α), b ∈ ⦃a⦄ → p b) ↔ p a

Universal membership over an atom reduces to its unique member. This is a routine property of multiset membership.

theorem Multiset.add_map_subset_map_filter_add_atom {α : Type u_1} {β : Type u_2} [DecidableEq α] (s : Multiset α) (t : Multiset β) (f : α → β) (a : α) : t + map f s ⊆ map f (filter (fun (x : α) => x ≠ a) s) + ⦃f a⦄ + t

After filtering out a, adjoining f a recovers every mapped member. This is a routine technical property of multiset membership.

theorem Multiset.map_subset_iff {α : Type u_1} {β : Type u_2} {s₁ s₂ : Multiset α} (f : α → β) (hf : Function.Injective f) : map f s₁ ⊆ map f s₂ ↔ s₁ ⊆ s₂

inductive Multiset.Traversal {α : Type u_1} : Multiset α → Type u_1

• zero {α : Type u_1} : Traversal 0
• succ {α : Type u_1} {s : Multiset α} (a : α) : s.Traversal → (s + ⦃a⦄).Traversal

def Multiset.Traversal.cast {α : Type u_1} {s t : Multiset α} (h : s = t) : s.Traversal → t.Traversal

Equations

• Multiset.Traversal.cast h t = h ▸ t

def Multiset.Traversal.atom {α : Type u_1} (a : α) : ⦃a⦄.Traversal

Equations

• Multiset.Traversal.atom a = Multiset.Traversal.succ a Multiset.Traversal.zero

def Multiset.Traversal.add {α✝ : Type u_1} {s₁ s₂ : Multiset α✝} (t₁ : s₁.Traversal) (t₂ : s₂.Traversal) : (s₁ + s₂).Traversal

Equations

• t₁.add Multiset.Traversal.zero = Multiset.Traversal.cast ⋯ t₁
• t₁.add (Multiset.Traversal.succ a t) = Multiset.Traversal.cast ⋯ (Multiset.Traversal.succ a (t₁.add t))

def Multiset.Traversal.toList {α : Type u_1} {s : Multiset α} : s.Traversal → List α

Equations

• Multiset.Traversal.zero.toList = []
• (Multiset.Traversal.succ a t).toList = a :: t.toList

theorem Multiset.Traversal.toList_cast {α : Type u_1} {s t : Multiset α} (h : s = t) (u : s.Traversal) : (cast h u).toList = u.toList

@[simp]

theorem Multiset.Traversal.coe_toList {α : Type u_1} {s : Multiset α} (t : s.Traversal) : ↑t.toList = s

def Multiset.Traversal.ofList {α : Type u_1} (l : List α) : (↑l).Traversal

Equations

• Multiset.Traversal.ofList [] = Multiset.Traversal.zero
• Multiset.Traversal.ofList (a :: t) = Multiset.Traversal.cast ⋯ (Multiset.Traversal.succ a (Multiset.Traversal.ofList t))

theorem Multiset.Traversal.toList_ofList {α : Type u_1} (l : List α) : (ofList l).toList = l

theorem Multiset.Traversal.ofList_toList {α : Type u_1} {s : Multiset α} (t : s.Traversal) : cast ⋯ (ofList t.toList) = t

def Multiset.Traversal.equiv {α : Type u_1} {s : Multiset α} : s.Traversal ≃ { l : List α // ↑l = s }

Equations

• One or more equations did not get rendered due to their size.

def Multiset.Traversal.map {α : Type u_1} {β : Type u_2} (f : α → β) {s : Multiset α} (t : s.Traversal) : (Multiset.map f s).Traversal

Construct a traversal after applying a function to every element.

Equations

• Multiset.Traversal.map f t = Multiset.Traversal.cast ⋯ (Multiset.Traversal.ofList (List.map f t.toList))

def Multiset.Traversal.filter {α : Type u_1} (p : α → Prop) [DecidablePred p] {s : Multiset α} (t : s.Traversal) : (Multiset.filter p s).Traversal

Construct a traversal of the elements satisfying a decidable predicate.

Equations

• Multiset.Traversal.filter p t = Multiset.Traversal.cast ⋯ (Multiset.Traversal.ofList (List.filter (fun (b : α) => decide (p b)) t.toList))

def Multiset.Traversal.erase {α : Type u_1} [DecidableEq α] (a : α) {s : Multiset α} (t : s.Traversal) : (s.erase a).Traversal

Construct a traversal after removing one occurrence of an element.

Equations

• Multiset.Traversal.erase a t = Multiset.Traversal.cast ⋯ (Multiset.Traversal.ofList (t.toList.erase a))

def Multiset.Traversal.remove {α : Type u_1} [DecidableEq α] {a : α} {s : Multiset α} (t : (s + ⦃a⦄).Traversal) : s.Traversal

Remove the distinguished occurrence from a traversal of an adjoined atom.

Equations

• t.remove = Multiset.Traversal.cast ⋯ (Multiset.Traversal.erase a t)

def Multiset.Traversal.getPreimage {β : Type u_1} {α : Type u_2} [DecidableEq β] {f : α → β} {s : Multiset α} (t : s.Traversal) {b : β} (h : b ∈ Multiset.map f s) : { a : α // a ∈ s ∧ f a = b }

Constructively extract a preimage from a mapped traversal.

Equations

• t.getPreimage h = ⟨↑(List.chooseX (fun (a : α) => f a = b) t.toList ⋯), ⋯⟩

@[instance_reducible]

noncomputable instance Multiset.Traversal.inhabited {α : Type u_1} {s : Multiset α} : Inhabited s.Traversal

Equations

• Multiset.Traversal.inhabited = { default := Multiset.Traversal.cast ⋯ (Multiset.Traversal.ofList s.toList) }