@[simp]
theorem
QuasiBorelSpace.Subtype.isHom_def
{A : Type u_1}
{x✝ : QuasiBorelSpace A}
{B : Type u_2}
{x✝¹ : QuasiBorelSpace B}
{P : B → Prop}
(f : A → Subtype P)
:
instance
QuasiBorelSpace.Subtype.instMeasurableQuasiBorelSpaceSubtype
{A : Type u_1}
{x✝ : QuasiBorelSpace A}
{P : A → Prop}
[MeasurableSpace A]
[MeasurableQuasiBorelSpace A]
:
theorem
QuasiBorelSpace.Subtype.isHom_mk
{A : Type u_1}
{x✝ : QuasiBorelSpace A}
{B : Type u_2}
{x✝¹ : QuasiBorelSpace B}
{P : B → Prop}
{f : A → B}
(hf₁ : IsHom f)
(hf₂ : ∀ (x : A), P (f x))
:
theorem
QuasiBorelSpace.Subtype.isHom_val
{A : Type u_1}
{x✝ : QuasiBorelSpace A}
{B : Type u_2}
{x✝¹ : QuasiBorelSpace B}
{P : B → Prop}
{f : A → Subtype P}
(hf : IsHom f)
:
IsHom fun (x : A) => ↑(f x)
def
OmegaQuasiBorelSpace.Subtype.subtype
{I : Type u_1}
{P : I → Prop}
[OmegaQuasiBorelSpace I]
(hP : ∀ (c : OmegaCompletePartialOrder.Chain I), (∀ i ∈ c, P i) → P (OmegaCompletePartialOrder.ωSup c))
:
Constructs an OmegaQuasiBorelSpace instance for a Subtype.
Equations
- OmegaQuasiBorelSpace.Subtype.subtype hP = { toOmegaCompletePartialOrder := OmegaCompletePartialOrder.subtype P hP, toQuasiBorelSpace := QuasiBorelSpace.Subtype.instSubtype, isHom_ωSup := ⋯ }