Documentation

QuasiBorelSpaces.Basic

theorem QuasiBorelSpace.isVar_cases {A : Type u_1} [QuasiBorelSpace A] {I : Type u_4} [Countable I] {ix : ℝ → I} {φ : I → ℝ → A} (hix : Measurable ix) (hφ : ∀ (n : I), IsVar (φ n)) :

IsVar fun (r : ℝ) => φ (ix r) r

@[simp]

theorem QuasiBorelSpace.isVar_iff_isHom {A : Type u_5} {x✝ : QuasiBorelSpace A} (f : ℝ → A) :

IsVar f ↔ IsHom f

@[simp]

theorem QuasiBorelSpace.isHom_ofMeasurableSpace {A : Type u_5} {x✝ : MeasurableSpace A} (φ : ℝ → A) :

IsHom φ ↔ Measurable φ

instance QuasiBorelSpace.instMeasurableQuasiBorelSpace {A : Type u_5} {x✝ : MeasurableSpace A} :

MeasurableQuasiBorelSpace A

theorem QuasiBorelSpace.isHom_def {A : Type u_5} {x✝ : QuasiBorelSpace A} {B : Type u_6} {x✝¹ : QuasiBorelSpace B} (f : A → B) :

IsHom f ↔ ∀ ⦃φ : ℝ → A⦄, IsHom φ → IsHom fun (x : ℝ) => f (φ x)

instance QuasiBorelSpace.IsHom.instCoeFunForallForallReal {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] {f : A → B} :

CoeFun (IsHom f) fun (x : IsHom f) => ∀ ⦃φ : ℝ → A⦄, IsHom φ → IsHom fun (x : ℝ) => f (φ x)

Equations

QuasiBorelSpace.IsHom.instCoeFunForallForallReal = { coe := ⋯ }

@[simp]

theorem QuasiBorelSpace.isHom_iff_measurable {A : Type u_5} [QuasiBorelSpace A] [MeasurableSpace A] [MeasurableQuasiBorelSpace A] (φ : ℝ → A) :

IsHom φ ↔ Measurable φ

theorem QuasiBorelSpace.isHom_of_measurable {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] [MeasurableSpace A] [MeasurableQuasiBorelSpace A] [MeasurableSpace B] [MeasurableQuasiBorelSpace B] (f : A → B) (hf : Measurable f) :

theorem QuasiBorelSpace.measurable_of_isHom {A : Type u_1} [QuasiBorelSpace A] [MeasurableSpace A] [MeasurableQuasiBorelSpace A] (f : ℝ → A) (hf : IsHom f) :

@[simp]

theorem QuasiBorelSpace.isHom_id {A : Type u_1} [QuasiBorelSpace A] :

@[simp]

theorem QuasiBorelSpace.isHom_id' {A : Type u_1} [QuasiBorelSpace A] :

IsHom fun (x : A) => x

theorem QuasiBorelSpace.isHom_comp {A : Type u_1} {B : Type u_2} {C : Type u_3} [QuasiBorelSpace A] [QuasiBorelSpace B] [QuasiBorelSpace C] {f : B → C} (hf : IsHom f) {g : A → B} (hg : IsHom g) :

IsHom (f ∘ g)

theorem QuasiBorelSpace.isHom_comp' {A : Type u_1} {B : Type u_2} {C : Type u_3} [QuasiBorelSpace A] [QuasiBorelSpace B] [QuasiBorelSpace C] {f : B → C} (hf : IsHom f) {g : A → B} (hg : IsHom g) :

IsHom fun (x : A) => f (g x)

@[simp]

theorem QuasiBorelSpace.isHom_const {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] (x : B) :

IsHom fun (x_1 : A) => x

theorem QuasiBorelSpace.isHom_cases {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] {I : Type u_4} [Countable I] {ix : A → I} {f : I → A → B} (hix : IsHom ix) (hf : ∀ (n : I), IsHom (f n)) :

IsHom fun (x : A) => f (ix x) x

@[simp]

theorem QuasiBorelSpace.isHom_of_discrete_countable {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] [MeasurableSpace A] [DiscreteQuasiBorelSpace A] [Countable A] (f : A → B) :

@[simp]

theorem QuasiBorelSpace.isHom_to_subsingleton {A : Type u_1} {B : Type u_2} [QuasiBorelSpace A] [QuasiBorelSpace B] [Subsingleton B] (f : A → B) :

theorem QuasiBorelSpace.isHom_of_lift {B : Type u_2} [QuasiBorelSpace B] {A : Type u_5} (f : A → B) :

theorem QuasiBorelSpace.isHom_to_lift {B : Type u_2} {C : Type u_3} [QuasiBorelSpace B] [QuasiBorelSpace C] {A : Type u_5} (f : A → B) (g : C → A) :

IsHom g ↔ IsHom fun (x : C) => f (g x)

@[simp]

theorem QuasiBorelSpace.isHom_unpack {A : Type u_1} [QuasiBorelSpace A] [Nonempty A] [MeasurableSpace A] [MeasurableQuasiBorelSpace A] [StandardBorelSpace A] :

IsHom MeasureTheory.unpack

theorem QuasiBorelSpace.isHom_cast {A : Type u_1} [QuasiBorelSpace A] {B : Type u_5} [instB : QuasiBorelSpace B] {C : Type u_5} [instC : QuasiBorelSpace C] {eq : B = C} (heq : ∀ (φ : ℝ → B), IsHom φ ↔ IsHom fun (x : ℝ) => cast eq (φ x)) (f : A → B) :

(IsHom fun (x : A) => cast eq (f x)) ↔ IsHom f