Commit 2026-08-13 08:29 fbb6fa0e

View on Github →

chore: rename Set.exists_mem_of_nonempty (#42546) Rename Set.exists_mem_of_nonempty to Set.exists_mem_univ_of_nonempty.

Estimated changes

Modified Mathlib/Data/Set/Basic.lean

deleted theorem Set.exists_mem_of_nonempty

added theorem Set.exists_mem_univ_of_nonempty

Modified Mathlib/LinearAlgebra/Multilinear/Basic.lean

Modified Mathlib/Topology/MetricSpace/GromovHausdorff.lean