Theorems · Theorem · category theory

CategoryTheory.Abelian.Pseudoelement.pseudoApply_aux

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q)
  (a b : CategoryTheory.Over P), a ≈ b → CategoryTheory.Abelian.app f a ≈ CategoryTheory.Abelian.app f b

If two elements are pseudo-equal, then their composition with a morphism is, too.

Defined in

Mathlib.CategoryTheory.Abelian.Pseudoelements

Cited by

0 results in Mathlib

Foundations

Depth 90 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Abelian