instance QuasiBorelSpace.Subtype.instSubtype {A : Type u_1} [QuasiBorelSpace A] {P : A → Prop} : QuasiBorelSpace (Subtype P)

Equations

• QuasiBorelSpace.Subtype.instSubtype = QuasiBorelSpace.lift Subtype.val

@[simp]

theorem QuasiBorelSpace.Subtype.isHom_def {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] {P : B → Prop} (f : A → Subtype P) : IsHom f ↔ IsHom fun (x : A) => ↑(f x)

instance QuasiBorelSpace.Subtype.instMeasurableQuasiBorelSpaceSubtype {A : Type u_1} [QuasiBorelSpace A] {P : A → Prop} [MeasurableSpace A] [MeasurableQuasiBorelSpace A] : MeasurableQuasiBorelSpace (Subtype P)

theorem QuasiBorelSpace.Subtype.isHom_mk {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] {P : B → Prop} {f : A → B} (hf₁ : IsHom f) (hf₂ : ∀ (x : A), P (f x)) : IsHom fun (x : A) => ⟨f x, ⋯⟩

theorem QuasiBorelSpace.Subtype.isHom_val {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] {P : B → Prop} {f : A → Subtype P} (hf : IsHom f) : IsHom fun (x : A) => ↑(f x)