Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-08 00:44 fe7cd33c

View on Github →

refactor(category_theory/products): tweak PR after merge

Estimated changes

Modified analysis/nnreal.lean

added def nnreal

Modified category_theory/functor.lean

added def category_theory.functor.comp

Modified category_theory/functor_category.lean

added theorem category_theory.functor.category.comp_app

added theorem category_theory.functor.category.id_app

added theorem category_theory.functor.category.nat_trans.app_naturality

added theorem category_theory.functor.category.nat_trans.naturality_app

deleted theorem category_theory.functor_category.comp_app

deleted theorem category_theory.functor_category.id_app

deleted theorem category_theory.functor_category.nat_trans.app_naturality

deleted theorem category_theory.functor_category.nat_trans.naturality_app

Modified category_theory/natural_transformation.lean

modified theorem category_theory.nat_trans.exchange

added def category_theory.nat_trans.hcomp

added def category_theory.nat_trans.vcomp

Modified category_theory/products.lean

added def category_theory.functor.prod

added theorem category_theory.functor.prod_map

added theorem category_theory.functor.prod_obj

deleted theorem category_theory.functor.product_map

deleted theorem category_theory.functor.product_obj

added def category_theory.nat_trans.prod

added theorem category_theory.nat_trans.prod_app

deleted theorem category_theory.nat_trans.product_app

added theorem category_theory.prod.category.comp

added def category_theory.prod.category.fst

added theorem category_theory.prod.category.id

added def category_theory.prod.category.inl

added def category_theory.prod.category.inr

added def category_theory.prod.category.snd

deleted theorem category_theory.product_category.comp

deleted theorem category_theory.product_category.id

Modified order/bounds.lean

added def is_glb

added def is_greatest

added def is_least

added def is_lub

added def lower_bounds

added def upper_bounds

Modified tactic/basic.lean