Documentation

LeanPool.QuasiBorelSpaces.Basic

LeanPool.QuasiBorelSpaces.Basic #

Imported Lean Pool material for LeanPool.QuasiBorelSpaces.Basic.

theorem QuasiBorelSpace.isVar_cases {A : Type u_1} {x✝ : 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_reducible]

instance QuasiBorelSpace.IsHom.instCoeFunForallForallReal {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : 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_1} {x✝ : QuasiBorelSpace A} {x✝¹ : MeasurableSpace A} [MeasurableQuasiBorelSpace A] (φ : ℝ → A) :

IsHom φ ↔ Measurable φ

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

@[simp]

theorem QuasiBorelSpace.isHom_id {A : Type u_1} {x✝ : QuasiBorelSpace A} :

@[simp]

theorem QuasiBorelSpace.isHom_id' {A : Type u_1} {x✝ : QuasiBorelSpace A} :

IsHom fun (x : A) => x

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

IsHom (Function.const A x)

@[simp]

theorem QuasiBorelSpace.isHom_const' {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} (x : B) :

IsHom fun (x_1 : A) => x

theorem QuasiBorelSpace.isHom_cases {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : 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} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {x✝² : MeasurableSpace A} [DiscreteQuasiBorelSpace A] [Countable A] (f : A → B) :

@[simp]

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

@[simp]

theorem QuasiBorelSpace.isHom_of_subsingleton {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} [Subsingleton A] (f : A → B) :

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

theorem QuasiBorelSpace.isHom_to_lift {B : Type u_2} {x✝ : QuasiBorelSpace B} {C : Type u_3} {x✝¹ : QuasiBorelSpace C} {A : Type u_5} (f : A → B) (g : C → A) :

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

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

IsHom MeasureTheory.unpack

theorem QuasiBorelSpace.isHom_mem_Icc {a b : ℝ} :

IsHom fun (x : ℝ) => x ∈ Set.Icc a b

theorem QuasiBorelSpace.isHom_cast {A : Type u_1} {x✝ : 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

theorem QuasiBorelSpace.measurable_of_isHom {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} {x✝² : MeasurableSpace A} [MeasurableQuasiBorelSpace A] {x✝³ : MeasurableSpace B} [MeasurableQuasiBorelSpace B] [StandardBorelSpace B] (f : B → A) (hf : IsHom f) :

theorem QuasiBorelSpace.NonEmpty.isHom_some {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_2} {x✝¹ : QuasiBorelSpace B} (f : ∀ (a : A), Nonempty B) :

IsHom fun (x : A) => ⋯.some

theorem QuasiBorelSpace.isHom_mono {A : Type u_1} {x✝ : QuasiBorelSpace A} {B : Type u_5} {f : A → B} {inst₁ inst₂ : QuasiBorelSpace B} (hf : IsHom f) (hinst : ∀ (φ : ℝ → B), IsVar φ → IsVar φ) :

theorem QuasiBorelSpace.measurableSet_toMeasurableSpace {A : Type u_1} {x✝ : QuasiBorelSpace A} (X : Set A) :

MeasurableSet X ↔ ∀ {φ : ℝ → A}, IsHom φ → MeasurableSet (φ ⁻¹' X)