Theorem CategoryTheory.Ind.isSeparating_range_yoneda

Modification history

2025-10-27 15:31
Mathlib/CategoryTheory/Generator/Indization.lean
refactor(CategoryTheory/Generator): use ObjectProperty instead of Set (#30269) …
Modified CategoryTheory.Ind.isSeparating_range_yonedaView on Github →
2025-01-27 06:10
Mathlib/CategoryTheory/Generator/Indization.lean
feat: separating set in the category of ind-objects (#21082) …
Added CategoryTheory.Ind.isSeparating_range_yonedaView on Github →