Theorem Set.Nonempty.exists_const

Modification history

2026-08-16 17:38
Mathlib/Data/Set/Basic.lean
chore(Data/Set): add missing `Set.forall_mem_*` lemmas (#42549) …
Added Set.Nonempty.exists_constView on Github →