Def SetLike.delabSubtypeSetLike

Modification history

2025-11-19 06:07
Mathlib/Data/SetLike/Basic.lean
chore: move Mathlib to the module system (#31786) …
Deleted SetLike.delabSubtypeSetLikeView on Github →
2023-10-25 17:26
Mathlib/Data/SetLike/Basic.lean
feat: pretty print as `↥S` instead of `{ x // x ∈ S }` for SetLike (#7927) …
Added SetLike.delabSubtypeSetLikeView on Github →