Def Set.Notation.delab_set_image_subtype

Modification history

2025-11-19 06:07
Mathlib/Data/Set/Notation.lean
chore: move Mathlib to the module system (#31786) …
Deleted Set.Notation.delab_set_image_subtypeView on Github →
2024-07-01 13:36
Mathlib/Data/Set/Functor.lean
chore: add exception for `Data.Set.Subset` to `noshake.json`. (#14196) …
Modified Set.Notation.delab_set_image_subtypeView on Github →
2024-03-03 21:54
Mathlib/Data/Set/Functor.lean
feat(Set): API for subset restriction and coercion to/from subtypes (#9940) …
Added Set.Notation.delab_set_image_subtypeView on Github →