Theorem Set.exists_mem_univ_of_nonempty

Modification history

2026-08-13 08:29
Mathlib/Data/Set/Basic.lean
chore: rename `Set.exists_mem_of_nonempty` (#42546) …
Added Set.exists_mem_univ_of_nonemptyView on Github →