Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-27 07:38 14c11403

View on Github →

chore(category_theory/groupoid/*) More subgroupoid lemmas (#17147) More subgroupoid lemmas and a few minor general cleanups.

Estimated changes

Modified src/category_theory/groupoid.lean

added theorem category_theory.groupoid.reverse_eq_inv

Modified src/category_theory/groupoid/free_groupoid.lean

modified def category_theory.free_groupoid

modified def category_theory.groupoid.free.of

Modified src/category_theory/groupoid/subgroupoid.lean

added theorem category_theory.subgroupoid.coe_inv_coe'

added theorem category_theory.subgroupoid.comap_comp

added theorem category_theory.subgroupoid.discrete_is_normal

added theorem category_theory.subgroupoid.galois_connection_map_comap

added theorem category_theory.subgroupoid.generated_le_generated_normal

added theorem category_theory.subgroupoid.id_mem_of_src

added theorem category_theory.subgroupoid.id_mem_of_tgt

added theorem category_theory.subgroupoid.inv_mem_iff

added theorem category_theory.subgroupoid.is_normal.generated_normal_le

modified structure category_theory.subgroupoid.is_normal

added theorem category_theory.subgroupoid.is_normal_map

added theorem category_theory.subgroupoid.is_wide.eq_to_hom_mem

added theorem category_theory.subgroupoid.is_wide.id_mem

added structure category_theory.subgroupoid.is_wide

added theorem category_theory.subgroupoid.is_wide_iff_objs_eq_univ

added theorem category_theory.subgroupoid.ker_comp

added theorem category_theory.subgroupoid.ker_is_normal

added theorem category_theory.subgroupoid.le_comap_map

added theorem category_theory.subgroupoid.map.arrows_iff

deleted theorem category_theory.subgroupoid.map.mem_arrows_iff

added theorem category_theory.subgroupoid.map_comap_le

added theorem category_theory.subgroupoid.map_le_iff_le_comap

added theorem category_theory.subgroupoid.map_objs_eq

added theorem category_theory.subgroupoid.mem_im_objs_iff

added theorem category_theory.subgroupoid.mem_map_iff

added theorem category_theory.subgroupoid.mem_map_objs_iff

added theorem category_theory.subgroupoid.mem_objs_of_src

added theorem category_theory.subgroupoid.mem_objs_of_tgt

added theorem category_theory.subgroupoid.mem_top

added theorem category_theory.subgroupoid.mem_top_objs

added theorem category_theory.subgroupoid.mul_mem_cancel_left

added theorem category_theory.subgroupoid.mul_mem_cancel_right

added theorem category_theory.subgroupoid.obj_surjective_of_im_eq_top

added theorem category_theory.subgroupoid.subset_generated