Equations
- One or more equations did not get rendered due to their size.
theorem
QuasiBorelSpace.Chain.isHom_apply
{A : Type u_1}
{x✝ : QuasiBorelSpace A}
[Preorder A]
(i : ℕ)
:
IsHom fun (f : OmegaCompletePartialOrder.Chain A) => f i
theorem
QuasiBorelSpace.Chain.isHom_pi
{A : Type u_1}
{x✝ : QuasiBorelSpace A}
{B : Type u_2}
{x✝¹ : QuasiBorelSpace B}
[Preorder B]
{f : A → OmegaCompletePartialOrder.Chain B}
(hf : ∀ (i : ℕ), IsHom fun (x : A) => (f x) i)
:
IsHom f
@[simp]
theorem
QuasiBorelSpace.Chain.isHom_iff
{A : Type u_1}
{x✝ : QuasiBorelSpace A}
{B : Type u_2}
{x✝¹ : QuasiBorelSpace B}
[Preorder B]
{f : A → OmegaCompletePartialOrder.Chain B}
: