Commit 2024-09-23 14:56 305ddf13

View on Github →

feat: maximal upper/minimal lower bounds of finset elements (#16970) Originally motivated by the Carleson project. We rename Finite.exists_ge_minimal to Finite.exists_minimal_le and add Finset and Set.Finite versions.

Estimated changes

Modified Mathlib/Data/Fintype/Order.lean

deleted theorem Finite.exists_ge_minimal

modified theorem Finite.exists_le_maximal

added theorem Finite.exists_minimal_le

added theorem Finset.exists_le_maximal

added theorem Finset.exists_minimal_le

added theorem Set.Finite.exists_le_maximal

added theorem Set.Finite.exists_minimal_le

Modified Mathlib/Order/Minimal.lean

modified theorem setOf_maximal_subset