Theorem Set.FiniteExhaustion.Set.nonempty_finiteExhaustion_iff

Modification history

2026-05-25 15:44
Mathlib/Data/Set/FiniteExhaustion.lean
fix: decls with a non-consecutive duplicate namespace (#39794) …
Deleted Set.FiniteExhaustion.Set.nonempty_finiteExhaustion_iffView on Github →
2025-12-12 15:51
Mathlib/Data/Set/FiniteExhaustion.lean
feat: FiniteExhaustion (#31921) …
Added Set.FiniteExhaustion.Set.nonempty_finiteExhaustion_iffView on Github →