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.

Author: YaelDillies

Mathlib/Order/Defs/Unbundled.lean

@@ -242,6 +242,26 @@ lemma Maximal.le_of_ge (h : Maximal P x) (hy : P y) (hge : x ≤ y) : y ≤ x :=
 
 end LE
 
+section LE
+variable {ι : Sort*} {α : Type*} [LE α] {P : ι → Prop} {f : ι → α} {i j : ι}
+
+/-- `Minimal P i` means that `i` is an element with minimal image along `f` satisfying `P`. -/
+def MinimalFor (P : ι → Prop) (f : ι → α) (i : ι) : Prop := P i ∧ ∀ ⦃j⦄, P j → f j ≤ f i → f i ≤ f j
+
+/-- `Maximal P i` means that `i` is an element with minimal image along `f` satisfying `P`. -/
+def MaximalFor (P : ι → Prop) (f : ι → α) (i : ι) : Prop := P i ∧ ∀ ⦃j⦄, P j → f i ≤ f j → f j ≤ f i
+
+lemma MinimalFor.prop (h : MinimalFor P f i) : P i := h.1
+lemma MaximalFor.prop (h : MaximalFor P f i) : P i := h.1
+
+lemma MinimalFor.le_of_le (h : MinimalFor P f i) (hj : P j) (hji : f j ≤ f i) : f i ≤ f j :=
+  h.2 hj hji
+
+lemma MaximalFor.le_of_le (h : MaximalFor P f i) (hj : P j) (hij : f i ≤ f j) : f j ≤ f i :=
+  h.2 hj hij
+
+end LE
+
 /-! ### Upper and lower sets -/
 
 /-- An upper set in an order `α` is a set such that any element greater than one of its members is

Mathlib/Order/Minimal.lean

@@ -34,7 +34,7 @@ but it may be worth re-examining this to make it easier in the future; see the T
 * `Finset` versions of the lemmas about sets.
 
 * API to allow for easily expressing min/maximality with respect to an arbitrary non-`LE` relation.
-
+* API for `MinimalFor`/`MaximalFor`
 -/
 
 assert_not_exists CompleteLattice