Documentation

LeanPool.QuasiBorelSpaces.Finset

LeanPool.QuasiBorelSpaces.Finset #

Imported Lean Pool material for LeanPool.QuasiBorelSpaces.Finset.

source
theorem QuasiBorelSpace.Finset.toSubtype_def {A : Type u_4} (x✝ : Finset A) :
toSubtype x✝ = match x✝ with | { val := x, nodup := h } => ⟨x, h⟩
source
@[irreducible]
def QuasiBorelSpace.Finset.toSubtype {A : Type u_4} :
Finset A → { xs : Multiset A // xs.Nodup }

View a finite set as its underlying nodup multiset.

Equations
Instances For
    source
    @[instance_reducible]
    instance QuasiBorelSpace.Finset.instFinset {A : Type u_1} [QuasiBorelSpace A] :
    QuasiBorelSpace (Finset A)
    Equations
    source
    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)
    source
    @[simp]
    theorem QuasiBorelSpace.Finset.isHom_singleton {A : Type u_1} [QuasiBorelSpace A] :
    IsHom fun (x : A) => {x}
    source
    @[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