Theorem Set.Finite.exists_le_maximal

Modification history

2024-09-23 14:56
Mathlib/Data/Fintype/Order.lean
feat: maximal upper/minimal lower bounds of finset elements (#16970) …
Added Set.Finite.exists_le_maximalView on Github →