iSupIndep_iff_supIndep — Mathlib

English

For a finite index set s, iSupIndep of f restricted to s is equivalent to s.SupIndep f.

Русский

Для конечного множества индексов s iSupIndep f ограниченного до s эквивалентно s.SupIndep f.

LaTeX

$$$\\\\forall s: Finset ι, {f : ι → α}, iSupIndep (f \\circ ((↑) : s → ι)) \\\\iff s.SupIndep f$$$

Lean4

theorem iSupIndep_iff_supIndep {s : Finset ι} {f : ι → α} : iSupIndep (f ∘ ((↑) : s → ι)) ↔ s.SupIndep f := by
  classical
  rw [Finset.supIndep_iff_disjoint_erase]
  refine Subtype.forall.trans (forall₂_congr fun a b => ?_)
  rw [Finset.sup_eq_iSup]
  congr! 1
  refine iSup_subtype.trans ?_
  congr! 1
  simp [iSup_and, @iSup_comm _ (_ ∈ s)]

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