Functors

This file provides basic lemmas about Functors and Sequences.

@[simp]

theorem QuasiBorelSpace.Functor.isHom_map {A B : Type u_2} {F : Type u_2 → Type u_1} {x✝ : QuasiBorelSpace A} {x✝¹ : QuasiBorelSpace B} [Functor F] (f : A → B) : IsHom (map f)

@[simp]

theorem QuasiBorelSpace.Functor.map_id {A : Type u_1} {F : Type u_1 → Type u_2} {x✝ : QuasiBorelSpace A} [Functor F] {f : A → A} (hf : ∀ (x : A), f x = x) (x : F A) : map f x = x

@[simp]

theorem QuasiBorelSpace.Functor.map_comp {A B C : Type u_1} {F : Type u_1 → Type u_2} {x✝ : QuasiBorelSpace A} {x✝¹ : QuasiBorelSpace B} {x✝² : QuasiBorelSpace C} [Functor F] {f : B → C} {g : A → B} (hf : IsHom f) (hg : IsHom g) (x : F A) : map f (map g x) = map (fun (x : A) => f (g x)) x

@[simp]

theorem QuasiBorelSpace.Sequence.isHom_map {S : ℕ → Type u_1} [Sequence S] {i j : ℕ} (h : i ≤ j) : IsHom (map h)

@[simp]

theorem QuasiBorelSpace.Sequence.map_id {S : ℕ → Type u_1} [Sequence S] {i : ℕ} (h : i ≤ i) (x : S i) : map h x = x

@[simp]

theorem QuasiBorelSpace.Sequence.map_comp {S : ℕ → Type u_1} [Sequence S] {j k i : ℕ} (h₁ : j ≤ k) (h₂ : i ≤ j) (x : S i) : map h₁ (map h₂ x) = map ⋯ x