Commit 2024-11-23 14:14 2abe270b

View on Github →

chore: rename Set.nonempty_of_nonempty_subtype to Set.Nonempty.of_subtype (#19408) This is shorter and allows anonymous dot notation. From GrowthInGroups (LeanCamCombi)

Estimated changes

Modified Mathlib/Data/ENat/Lattice.lean

Modified Mathlib/Data/Set/Basic.lean

added theorem Set.Nonempty.of_subtype

deleted theorem Set.nonempty_of_nonempty_subtype

Modified Mathlib/Data/Set/Image.lean

Modified Mathlib/GroupTheory/PGroup.lean