mathlib3 documentation

category_theory.concrete_category.elementwise

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we provide various simp lemmas in its elementwise form via tactic.elementwise.

@[simp]
theorem category_theory.limits.cocone.w_apply {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] {F : J C} (c : category_theory.limits.cocone F) {j j' : J} (f : j j') [I : category_theory.concrete_category C] (x : (F.obj j)) :
(c.ι.app j') ((F.map f) x) = (c.ι.app j) x
@[simp]
theorem category_theory.limits.cone.w_apply {J : Type u₁} [category_theory.category J] {C : Type u₃} [category_theory.category C] {F : J C} (c : category_theory.limits.cone F) {j j' : J} (f : j j') [I : category_theory.concrete_category C] (x : (((category_theory.functor.const J).obj c.X).obj j)) :
(F.map f) ((c.π.app j) x) = (c.π.app j') x