Commit 2025-04-18 17:03 af881a91

feat: minimality with respect to a function (#23706) Introduce MinimalFor/MaximalFor, which generalise Minimal and Maximal to the case where the predicate P : ι → Prop doesn't have an ordered domain, but where instead we have a function f : ι → α to an order. Typical examples include extremal properties of graphs, such as Simple.IsTuran.Maximal, where we don't just care about having a maximal clique-free graph, but we also want it to have the maximal number of edges.