Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-27 05:47 61095582

View on Github →

chore(category_theory/*): provide aliases quiver.hom.le and has_le.le.hom (#7677)

Estimated changes

Modified src/algebra/category/Module/limits.lean

Modified src/category_theory/category/default.lean

modified theorem category_theory.hom_of_le_le_of_hom

modified theorem category_theory.hom_of_le_refl

modified theorem category_theory.le_of_hom_hom_of_le

Modified src/category_theory/category/pairwise.lean

Modified src/category_theory/equivalence.lean

Modified src/category_theory/functor.lean

Modified src/category_theory/isomorphism.lean

modified theorem category_theory.iso.to_eq

Modified src/category_theory/limits/lattice.lean

Modified src/category_theory/opposites.lean

modified theorem category_theory.le_of_op_hom

modified def category_theory.op_hom_of_le

Modified src/category_theory/sites/spaces.lean

Modified src/category_theory/skeletal.lean

Modified src/category_theory/subobject/basic.lean

Modified src/category_theory/subobject/lattice.lean

Modified src/category_theory/subobject/types.lean

Modified src/topology/category/Profinite/as_limit.lean

Modified src/topology/category/Top/limits.lean

Modified src/topology/category/Top/open_nhds.lean

Modified src/topology/category/Top/opens.lean

modified def topological_space.opens.bot_le

modified def topological_space.opens.inf_le_left

modified def topological_space.opens.inf_le_right

modified def topological_space.opens.le_supr

modified def topological_space.opens.le_top

Modified src/topology/sheaves/local_predicate.lean

Modified src/topology/sheaves/sheaf_condition/opens_le_cover.lean

Modified src/topology/sheaves/sheaf_condition/unique_gluing.lean