class QuasiBorelSpace.IsHomDiagonal (A : Type u_3) [QuasiBorelSpace A] : Prop

The class of QuasiBorelSpaces where equality is a morphism.

• isHom_eq : IsHom fun (x : A × A) => x.1 = x.2

  Equality is a morphism.

theorem QuasiBorelSpace.isHom_eq' {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] [IsHomDiagonal B] {f g : A → B} (hf : IsHom f) (hg : IsHom g) : IsHom fun (x : A) => f x = g x

instance QuasiBorelSpace.instIsHomDiagonalOfCountableOfDiscreteQuasiBorelSpace {A : Type u_1} [Countable A] [MeasurableSpace A] [QuasiBorelSpace A] [DiscreteQuasiBorelSpace A] : IsHomDiagonal A

instance QuasiBorelSpace.instIsHomDiagonalProd {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] [IsHomDiagonal A] [IsHomDiagonal B] : IsHomDiagonal (A × B)

instance QuasiBorelSpace.instIsHomDiagonalSum {A : Type u_1} [QuasiBorelSpace A] {B : Type u_2} [QuasiBorelSpace B] [IsHomDiagonal A] [IsHomDiagonal B] : IsHomDiagonal (A ⊕ B)

instance QuasiBorelSpace.instIsHomDiagonalReal : IsHomDiagonal ℝ