English
If t is SupIndep and s ⊆ t, then s is SupIndep with the same f.
Русский
Если t является SupIndep и s ⊆ t, то s также SupIndep с тем же f.
LaTeX
$$$\\text{SupIndep}(t,f) \\land s \\subseteq t \\Rightarrow \\text{SupIndep}(s,f).$$$
Lean4
/-- If both the index type and the lattice have decidable equality,
then the `SupIndep` predicate is decidable.
TODO: speedup the definition and drop the `[DecidableEq ι]` assumption
by iterating over the pairs `(a, t)` such that `s = Finset.cons a t _`
using something like `List.eraseIdx`
or by generating both `f i` and `(s.erase i).sup f` in one loop over `s`.
Yet another possible optimization is to precompute partial suprema of `f`
over the inits and tails of the list representing `s`,
store them in 2 `Array`s,
then compute each `sup` in 1 operation. -/
instance [DecidableEq ι] [DecidableEq α] : Decidable (SupIndep s f) :=
have : ∀ i, Decidable (Disjoint (f i) ((s.erase i).sup f)) := fun _ ↦ decidable_of_iff _ disjoint_iff.symm
decidable_of_iff _ supIndep_iff_disjoint_erase.symm
