instance QuasiBorelSpace.Finset.instFinset {A : Type u_1} [QuasiBorelSpace A] : QuasiBorelSpace (Finset A)

Equations

• QuasiBorelSpace.Finset.instFinset = QuasiBorelSpace.lift QuasiBorelSpace.Finset.toSubtype✝

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

@[simp]

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

@[simp]

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