mathlib

31ba155f - feat(algebraic_topology/cech_nerve): The Cech nerve is a right adjoint. (#7716)

feat(algebraic_topology/cech_nerve): The Cech nerve is a right adjoint. (#7716) Also fixes the namespace in the file `algebraic_topology/cech_nerve.lean`. This is needed for LTE Co-authored-by: Scott Morrison <scott.morrison@gmail.com>