mathlib3

239d882c - refactor(category_theory/epi_mono): is_split_epi and split_epi (#16036)

refactor(category_theory/epi_mono): is_split_epi and split_epi (#16036) This PR makes a distinction between the class `is_split_epi f` which is a `Prop` and `split_epi f` which contains the datum of a section of `f`.