splitSetByVarSign — Mathlib

Lean4
/-- `splitSetByVarSign a comps` partitions the set `comps` into three parts.
* `pos` contains the elements of `comps` in which `a` has a positive coefficient.
* `neg` contains the elements of `comps` in which `a` has a negative coefficient.
* `notPresent` contains the elements of `comps` in which `a` has coefficient 0.

Returns `(pos, neg, notPresent)`.
-/
def splitSetByVarSign (a : ℕ) (comps : PCompSet) : PCompSet × PCompSet × PCompSet :=
  comps.foldl
    (fun ⟨pos, neg, notPresent⟩ pc =>
      let n := pc.c.coeffOf a
      if n > 0 then ⟨pos.insert pc, neg, notPresent⟩
      else if n < 0 then ⟨pos, neg.insert pc, notPresent⟩ else ⟨pos, neg, notPresent.insert pc⟩)
    ⟨TreeSet.empty, TreeSet.empty, TreeSet.empty⟩
Похожие утверждения