instance QuasiBorelSpace.Multiset.instMultiset {A : Type u_1} [QuasiBorelSpace A] : QuasiBorelSpace (Multiset A)

Equations

• QuasiBorelSpace.Multiset.instMultiset = QuasiBorelSpace.lift fun (x : Quotient (List.isSetoid A)) => x

theorem QuasiBorelSpace.Multiset.isHom_fold {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] {op : A → B → B → B} [∀ (x : A), Std.Commutative (op x)] [∀ (x : A), Std.Associative (op x)] (hop : IsHom fun (x : A × B × B) => match x with | (x, y, z) => op x y z) (z : A → B) (hz : IsHom z) (f : A → Multiset B) (hf : IsHom f) : IsHom fun (x : A) => Multiset.fold (op x) (z x) (f x)

@[simp]

theorem QuasiBorelSpace.Multiset.isHom_ofList {A : Type u_1} [QuasiBorelSpace A] : IsHom Multiset.ofList

@[simp]

theorem QuasiBorelSpace.Multiset.isHom_add {A : Type u_1} [QuasiBorelSpace A] : IsHom fun (x : Multiset A × Multiset A) => x.1 + x.2

@[simp]

theorem QuasiBorelSpace.Multiset.isHom_sub {A : Type u_1} [QuasiBorelSpace A] [DecidableEq A] [IsHomDiagonal A] : IsHom fun (x : Multiset A × Multiset A) => x.1 - x.2

@[simp]

theorem QuasiBorelSpace.Multiset.isHom_union {A : Type u_1} [QuasiBorelSpace A] [DecidableEq A] [IsHomDiagonal A] : IsHom fun (x : Multiset A × Multiset A) => x.1 ∪ x.2

@[simp]

theorem QuasiBorelSpace.Multiset.isHom_ndunion {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] [DecidableEq B] [IsHomDiagonal B] {f : A → Multiset B} (hf : IsHom f) {g : A → Multiset B} (hg : IsHom g) : IsHom fun (x : A) => (f x).ndunion (g x)

@[simp]

theorem QuasiBorelSpace.Multiset.isHom_cons {A : Type u_1} [QuasiBorelSpace A] : IsHom fun (x : A × Multiset A) => x.1 ::ₘ x.2

@[simp]

theorem QuasiBorelSpace.Multiset.isHom_singleton {A : Type u_1} [QuasiBorelSpace A] : IsHom fun (x : A) => {x}

@[simp]

theorem QuasiBorelSpace.Multiset.isHom_map {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] {C : Type u_3} [QuasiBorelSpace C] {f : A → B → C} (hf : IsHom fun (x : A × B) => match x with | (x, y) => f x y) {g : A → Multiset B} (hg : IsHom g) : IsHom fun (x : A) => Multiset.map (f x) (g x)