Mathlib v3 is deprecated. Go to Mathlib v4

Theorem set.exists_mem_of_nonempty

Modification history

2018-12-24 20:12
data/set/basic.lean
feat(analysis/topology): miscellaneous topology (#484) …
Added set.exists_mem_of_nonemptyView on Github →