Supporting results for pointwise provable equality.

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

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

Equations

• ⦃a⦄ = {a}

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

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

Equations

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

def PointwiseComposition.Multiset.pairUnexpander : Lean.PrettyPrinter.Unexpander

The pair Unexpander construction in Multiset.

Equations

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem PointwiseComposition.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.

theorem PointwiseComposition.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 PointwiseComposition.Multiset.add_map_subset_map_filter_add_atom {α : Type u_1} {β : Type u_2} [DecidableEq α] (s : Multiset α) (t : Multiset β) (f : α → β) (a : α) : t + Multiset.map f s ⊆ Multiset.map f (Multiset.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 PointwiseComposition.Multiset.map_subset_iff {α : Type u_1} {β : Type u_2} {s₁ s₂ : Multiset α} (f : α → β) (hf : Function.Injective f) : Multiset.map f s₁ ⊆ Multiset.map f s₂ ↔ s₁ ⊆ s₂

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

Data and laws for Traversal in Multiset.

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

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

The cast construction in Multiset.Traversal.

Equations

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

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

The atom construction in Multiset.Traversal.

Equations

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

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

The add construction in Multiset.Traversal.

Equations

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

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

The to List construction in Multiset.Traversal.

Equations

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

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

@[simp]

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

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

The of List construction in Multiset.Traversal.

Equations

• One or more equations did not get rendered due to their size.
• PointwiseComposition.Multiset.Traversal.ofList [] = PointwiseComposition.Multiset.Traversal.zero

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

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

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

The equiv construction in Multiset.Traversal.

Equations

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

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

Construct a traversal after applying a function to every element.

Equations

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

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

Construct a traversal of the elements satisfying a decidable predicate.

Equations

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

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

Construct a traversal after removing one occurrence of an element.

Equations

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

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

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

Equations

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

def PointwiseComposition.Multiset.Traversal.getPreimage {β : Type u_1} {α : Type u_2} [DecidableEq β] {f : α → β} {s : Multiset α} (t : Traversal s) {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 PointwiseComposition.Multiset.Traversal.inhabited {α : Type u_1} {s : Multiset α} : Inhabited (Traversal s)

Equations

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