Quotients of Quasi-Borel Spaces

This file defines a QuasiBorelSpace instance for Quotients.

@[instance_reducible]

instance QuasiBorelSpace.Quotient.instQuotient {A : Type u_1} {S : Setoid A} [QuasiBorelSpace 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} {S : Setoid A} [QuasiBorelSpace A] (φ : ℝ → Quotient S) : IsVar φ = ∃ (ψ : ℝ → A), IsHom ψ ∧ ∀ (r : ℝ), φ r = ⟦ψ r⟧

@[simp]

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

@[simp]

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

theorem QuasiBorelSpace.Quotient.isHom_lift {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {C : Type u_3} {x✝² : 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)

@[simp]

theorem QuasiBorelSpace.Quotient.isHom_map {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {S : Setoid A} {S' : Setoid B} {f : A → B} (hf₁ : ∀ ⦃a b : A⦄, a ≈ b → f a ≈ f b) (hf₂ : IsHom f) : IsHom (Quotient.map f hf₁)

theorem QuasiBorelSpace.Quotient.isHom_choice {I : Type u_5} {P : I → Type u_4} [(i : I) → QuasiBorelSpace (P i)] {S : (i : I) → Setoid (P i)} : IsHom Quotient.choice

theorem QuasiBorelSpace.Quotient.isHom_eval {I : Type u_5} {P : I → Type u_4} [(i : I) → QuasiBorelSpace (P i)] {S : (i : I) → Setoid (P i)} : IsHom Quotient.eval

theorem QuasiBorelSpace.Quotient.induction_on_hom {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {S : Setoid A} {P : (B →𝒒 Quotient S) → Prop} [MeasurableSpace B] [MeasurableQuasiBorelSpace B] [StandardBorelSpace B] (mk : ∀ (φ : B →𝒒 A), P { toFun := fun (x : B) => ⟦φ x⟧, property := ⋯ }) (f : B →𝒒 Quotient S) : P f

noncomputable def QuasiBorelSpace.Quotient.homChoice {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {S : Setoid A} [MeasurableSpace B] [MeasurableQuasiBorelSpace B] [StandardBorelSpace B] (f : B →𝒒 Quotient S) : Quotient inferInstance

Equations

• QuasiBorelSpace.Quotient.homChoice f = ⟦QuasiBorelSpace.Quotient.subvar✝ ⇑f⟧

@[simp]

theorem QuasiBorelSpace.Quotient.homChoice_eq {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {S : Setoid A} [MeasurableSpace B] [MeasurableQuasiBorelSpace B] [StandardBorelSpace B] (f : B →𝒒 A) : homChoice { toFun := fun (x : B) => ⟦f x⟧, property := ⋯ } = ⟦f⟧

@[simp]

theorem QuasiBorelSpace.Quotient.homChoice_eq' {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {S : Setoid A} [MeasurableSpace B] [MeasurableQuasiBorelSpace B] [StandardBorelSpace B] {f : B → A} (hf : IsHom f) : homChoice { toFun := fun (x : B) => ⟦f x⟧, property := ⋯ } = ⟦{ toFun := f, property := hf }⟧

@[simp]

theorem QuasiBorelSpace.Quotient.isHom_homChoice {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {S : Setoid A} [MeasurableSpace B] [MeasurableQuasiBorelSpace B] [StandardBorelSpace B] : IsHom homChoice