Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-02 15:11 71ef45e2

View on Github →

chore(topology/sheaves): depend less on rfl (#3994) Another backport from the prop_limits branch.

Estimated changes

Modified src/category_theory/limits/shapes/types.lean

deleted theorem category_theory.limits.types.lift_π_apply'

added theorem category_theory.limits.types.pi_lift_π_apply

added theorem category_theory.limits.types.pi_map_π_apply

Modified src/category_theory/limits/types.lean

added theorem category_theory.limits.types.colimit_sound

added theorem category_theory.limits.types.colimit_w_apply

added theorem category_theory.limits.types.filtered_colimit.colimit_eq_iff_aux

added theorem category_theory.limits.types.limit_w_apply

added theorem category_theory.limits.types.map_π_apply

added theorem category_theory.limits.types.ι_map_apply

Modified src/topology/sheaves/local_predicate.lean

Modified src/topology/sheaves/stalks.lean