mathlib
15b6c56a - refactor(category_theory/limits/types): Refactor filtered colimits. (#9100)

Commit
4 years ago
refactor(category_theory/limits/types): Refactor filtered colimits. (#9100) - Rename `filtered_colimit.r` into `filtered_colimit.rel`, to match up with `quot.rel`, - Rename lemma `r_ge`, - Abstract out lemma `eqv_gen_quot_rel_of_rel` from later proof.
Parents
Loading