feat(Combinatorics/SimpleGraph/Finite): LocallyFiniteOrder

Adds the order-theoretic local-finiteness of `SimpleGraph V` (every `Icc G H`
is a `Finset`), distinct from the existing graph-theoretic `LocallyFinite`
(every vertex has a finite neighborhood) elsewhere in the file.

* `SimpleGraph.decidableLE` (instance): `G ≤ H` is decidable under `[Fintype V]`
  and per-graph adjacency decidability `[DecidableRel G.Adj] [DecidableRel H.Adj]`.
* `SimpleGraph.locallyFiniteOrder` (non-instance abbrev): produces
  `LocallyFiniteOrder (SimpleGraph V)` under
  `[Fintype V] [DecidableEq V] [DecidableLE (SimpleGraph V)]`, built via
  `LocallyFiniteOrder.ofIcc'`.

The abbrev is deliberately not an instance — `DecidableLE (SimpleGraph V)`
cannot be synthesised globally because `DecidableRel G.Adj` is value-dependent.
Callers either compose `decidableLE` after providing per-graph adjacency
decidability, or use `letI := Classical.decRel _` for a noncomputable order.

Required downstream for `Finset.Icc G ⊤` in the Möbius inversion between copy
counts and induced copy counts.

Author: FordUniver

Mathlib/Combinatorics/SimpleGraph/Finite.lean

@@ -8,6 +8,7 @@ module
 public import Mathlib.Combinatorics.SimpleGraph.Maps
 public import Mathlib.Data.Finset.Max
 public import Mathlib.Data.Sym.Card
+public import Mathlib.Order.Interval.Finset.Defs
 
 /-!
 # Definitions for finite and locally finite graphs
@@ -529,6 +530,25 @@ theorem card_commonNeighbors_top [DecidableEq V] {v w : V} (h : v ≠ w) :
 
 end Finite
 
+section LocallyFiniteOrder
+
+variable [Fintype V]
+
+/-- `G ≤ H` is decidable when adjacency is decidable on both sides. -/
+instance decidableLE {G H : SimpleGraph V}
+    [DecidableRel G.Adj] [DecidableRel H.Adj] : Decidable (G ≤ H) :=
+  decidable_of_iff (∀ v w, G.Adj v w → H.Adj v w) Iff.rfl
+
+/-- The lattice of simple graphs on a finite type is locally finite when the order is
+decidable. -/
+instance [DecidableEq V] [DecidableLE (SimpleGraph V)] :
+    LocallyFiniteOrder (SimpleGraph V) :=
+  LocallyFiniteOrder.ofIcc' (SimpleGraph V)
+    (fun G₁ G₂ => {G | G₁ ≤ G ∧ G ≤ G₂})
+    (fun _ _ _ => by simp)
+
+end LocallyFiniteOrder
+
 namespace Iso
 
 variable {G} {W : Type*} {G' : SimpleGraph W}