theorem QuasiBorelSpace.ENNReal.isHom_add {A : Type u_1} {x✝ : QuasiBorelSpace A} {f : A → ENNReal} (hf : IsHom f) {g : A → ENNReal} (hg : IsHom g) : IsHom fun (x : A) => f x + g x

theorem QuasiBorelSpace.ENNReal.isHom_mul {A : Type u_1} {x✝ : QuasiBorelSpace A} {f : A → ENNReal} (hf : IsHom f) {g : A → ENNReal} (hg : IsHom g) : IsHom fun (x : A) => f x * g x

theorem QuasiBorelSpace.ENNReal.isHom_iSup {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} [Countable B] {f : A → B → ENNReal} (hf : ∀ (b : B), IsHom fun (x : A) => f x b) : IsHom fun (x : A) => ⨆ (i : B), f x i

noncomputable instance OmegaQuasiBorelSpace.ENNReal.instENNReal : OmegaQuasiBorelSpace ENNReal

ωQBS structure on ENNReal

Equations

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