supIndep_iff_pairwiseDisjoint — Mathlib

English

For a finite set s of indices, SupIndep with respect to f is equivalent to pairwise disjointness of the family {f(i) | i ∈ s}.

Русский

Для конечного множества индексов s SupIndep относительно f эквивалентно попарно непересечности семейства {f(i) | i∈s}.

LaTeX

$$$s.SupIndep f \\iff (s : Set ι).PairwiseDisjoint f$$$

Lean4

theorem supIndep_iff_pairwiseDisjoint : s.SupIndep f ↔ (s : Set ι).PairwiseDisjoint f :=
  ⟨SupIndep.pairwiseDisjoint, fun hs _ ht _ hi hit =>
    Finset.disjoint_sup_right.2 fun _ hj => hs hi (ht hj) (ne_of_mem_of_not_mem hj hit).symm⟩

Похожие утверждения