chore: split Data.Ordmap.Ordset (#23529)

The constituent parts of the invariant have been pushed backwards to `Data.Ordmap.Invariants`. The bundled `Valid` predicate and `Ordset` itself remain in place.

Author: Parcly-Taxel

Mathlib.lean

@@ -3150,6 +3150,7 @@ import Mathlib.Data.Option.Defs
 import Mathlib.Data.Option.NAry
 import Mathlib.Data.Ordering.Basic
 import Mathlib.Data.Ordering.Lemmas
+import Mathlib.Data.Ordmap.Invariants
 import Mathlib.Data.Ordmap.Ordnode
 import Mathlib.Data.Ordmap.Ordset
 import Mathlib.Data.PEquiv