Theorem Set.image_coe_eq_restrict_image

Modification history

2024-04-14 10:41

Mathlib/Data/Set/Functor.lean

chore: remove autoImplicit from more files (#11798) …

Modified Set.image_coe_eq_restrict_image View on Github →

2023-08-09 19:01

Mathlib/Data/Set/Functor.lean

feat(Topology/ExtremallyDisconnected): prove Gleason's theorem (#5634) …

Added Set.image_coe_eq_restrict_image View on Github →