Graph theory def: Maximal/maximum cliques & independent sets

We have SimpleGraph.IsClique and SimpleGraph.IsIndepSet for cliques & independent sets in simple graphs.

We also have SimpleGraph.IsMaximumClique and SimpleGraph.IsMaximumIndepSet for the maximum versions.

The file Mathlib.Combinatorics.SimpleGraph.Clique also proves things about the maximal versions, using Maximal G.IsClique s and Maximal G.IsIndepSet s inline while naming theorems with "isMaximalClique" and "isMaximalIndepSet".

I suggest we're missing the following defs:

open Cardinal

def IsMaximalClique (G : SimpleGraph V) (s : Set V) :=
  Maximal G.IsClique s

def IsMaximumClique (G : SimpleGraph V) (s : Set V) :=
  MaximalFor G.IsClique (#·) s

def IsMaximalIndepSet (G : SimpleGraph V) (s : Set V) :=
  Maximal G.IsIndepSet s

def IsMaximumIndepSet (G : SimpleGraph V) (s : Set V) :=
  MaximalFor G.IsIndepSet (#·) s

where the maximum versions are intended to replace the existing structures with the same name.

I think not having the maximal versions is hurting Loogle-ability, and that we should use Maximal/MaximalFor where possible to gain access to useful API.

Start in Mathlib/Combinatorics/SimpleGraph/Clique, where maximal clique and independent-set properties are currently used inline and maximum versions already exist. Review the existing theorems and structures, then check references to the current maximum definitions before adding the proposed names and updating their uses. Done means the definitions are available for Loogle and the relevant mathlib checks pass.