iSupIndep_iff_supIndep_univ — Mathlib

English

For a finite index type ι, iSupIndep f is equivalent to Finset.univ.SupIndep f.

Русский

Для конечного типа индексов ι iSupIndep f эквивалентно Finset.univ.SupIndep f.

LaTeX

$$$iSupIndep f \\\\iff Finset.univ.SupIndep f$$$

Lean4

/-- A variant of `CompleteLattice.iSupIndep_iff_supIndep` for `Fintype`s. -/
theorem iSupIndep_iff_supIndep_univ [Fintype ι] {f : ι → α} : iSupIndep f ↔ Finset.univ.SupIndep f := by
  classical simp [Finset.supIndep_iff_disjoint_erase, iSupIndep, Finset.sup_eq_iSup]

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