@[simp]

theorem Rose.Encoding.isHom_mk {A : Type u_1} [QuasiBorelSpace A] : QuasiBorelSpace.IsHom fun (x : A × List (Encoding A)) => mk x.1 x.2

theorem Rose.Encoding.isHom_fold {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] {mk : A → List B → B} (hmk : QuasiBorelSpace.IsHom fun (x : A × List B) => match x with | (x, y) => mk x y) : QuasiBorelSpace.IsHom (fold mk)

instance QuasiBorelSpace.Rose.instRose {A : Type u_1} [QuasiBorelSpace A] : QuasiBorelSpace (Rose A)

Equations

• QuasiBorelSpace.Rose.instRose = QuasiBorelSpace.lift Rose.Encoding.encode

@[simp]

theorem QuasiBorelSpace.Rose.isHom_encode {A : Type u_1} [QuasiBorelSpace A] : IsHom Rose.Encoding.encode

theorem QuasiBorelSpace.Rose.isHom_mk {A : Type u_1} [QuasiBorelSpace A] : IsHom fun (x : A × List (Rose A)) => { label := x.1, children := x.2 }

theorem QuasiBorelSpace.Rose.isHom_cons' {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] {f : A → B} (hf : IsHom f) {g : A → List (Rose B)} (hg : IsHom g) : IsHom fun (x : A) => { label := f x, children := g x }

theorem QuasiBorelSpace.Rose.isHom_fold {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] {mk : A → List B → B} (hmk : IsHom fun (x : A × List B) => match x with | (x, xs) => mk x xs) : IsHom (Rose.fold mk)

theorem QuasiBorelSpace.Rose.isHom_fold' {A : Type u_1} {B : Type u_2} {C : Type u_3} [QuasiBorelSpace A] [QuasiBorelSpace B] [QuasiBorelSpace C] {mk : A → B → List C → C} (hmk : IsHom fun (x : A × B × List C) => match x with | (x, y, z) => mk x y z) {f : A → Rose B} (hf : IsHom f) : IsHom fun (x : A) => Rose.fold (mk x) (f x)

@[simp]

theorem QuasiBorelSpace.Rose.isHom_label {A : Type u_1} [QuasiBorelSpace A] : IsHom fun (t : Rose A) => t.label

@[simp]

theorem QuasiBorelSpace.Rose.isHom_children {C : Type u_3} [QuasiBorelSpace C] : IsHom fun (t : Rose C) => t.children

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

instance QuasiBorelSpace.Rose.instSeparatesPointsRose {A : Type u_1} [QuasiBorelSpace A] [SeparatesPoints A] : SeparatesPoints (Rose A)