Mathlib v3 is deprecated. Go to Mathlib v4

Def category_theory.glue_data.sigma_opens

Modification history

2021-12-18 10:22
src/category_theory/glue_data.lean
feat(category_theory): Glue data (#10436)
Added category_theory.glue_data.sigma_opensView on Github →