English
SupIndep is the property that for every subset t of s and every i in s but not in t, f(i) is disjoint from the supremum of f over t.
Русский
SupIndep—свойство: для любого подмножества t ⊆ s и любого элемента i ∈ s, которого нет в t, f(i) несовместен с t.sup f.
LaTeX
$$$\\operatorname{SupIndep}(s,f) := \\forall t \\subseteq s, \\forall i \\in s, i \\notin t \\Rightarrow \\operatorname{Disjoint}(f(i), t.sup f).$$$
Lean4
/-- Supremum independence of finite sets. We avoid the "obvious" definition using `s.erase i`
because `erase` would require decidable equality on `ι`. -/
def SupIndep (s : Finset ι) (f : ι → α) : Prop :=
∀ ⦃t⦄, t ⊆ s → ∀ ⦃i⦄, i ∈ s → i ∉ t → Disjoint (f i) (t.sup f)
