instance QuasiBorelSpace.Quotient.instQuotient {A : Type u_1} [QuasiBorelSpace A] {S : Setoid A} : QuasiBorelSpace (Quotient S)

Equations

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

@[simp]

theorem QuasiBorelSpace.Quotient.IsVar_def {A : Type u_1} [QuasiBorelSpace A] {S : Setoid A} (φ : ℝ → Quotient S) : IsVar φ = ∃ (ψ : ℝ → A), IsHom ψ ∧ ∀ (r : ℝ), φ r = ⟦ψ r⟧

@[simp]

theorem QuasiBorelSpace.Quotient.isHom_def {A : Type u_1} [QuasiBorelSpace A] {S : Setoid A} (φ : ℝ → Quotient S) : IsHom φ ↔ ∃ (ψ : ℝ → A), IsHom ψ ∧ ∀ (r : ℝ), φ r = ⟦ψ r⟧

@[simp]

theorem QuasiBorelSpace.Quotient.isHom_mk {A : Type u_1} [QuasiBorelSpace A] {S : Setoid A} : IsHom fun (x : A) => ⟦x⟧

@[simp]

theorem QuasiBorelSpace.Quotient.isHom_lift {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] {S : Setoid A} {f : A → B} (hf₁ : IsHom f) (hf₂ : ∀ (x y : A), x ≈ y → f x = f y) : IsHom (Quotient.lift f hf₂)

@[simp]

theorem QuasiBorelSpace.Quotient.isHom_lift' {A : Type u_1} {B : Type u_2} {C : Type u_3} [QuasiBorelSpace A] [QuasiBorelSpace B] [QuasiBorelSpace C] {S : Setoid A} {f : C → A → B} (hf₁ : IsHom fun (x : C × A) => match x with | (x, y) => f x y) (hf₂ : ∀ (x : C) (y z : A), y ≈ z → f x y = f x z) {g : C → Quotient S} (hg : IsHom g) : IsHom fun (x : C) => Quotient.lift (f x) ⋯ (g x)