English
Let β be a family of type indices β(i). If each slice (g i).sup with f on pairs is SupIndep and the fibers themselves are SupIndep, then the sigma-construction (s.sigma g) yields SupIndep for f.
Русский
Пусть β : i → Type и для каждого i задано Finset (β i). Если соответственно для каждой i условие SupIndep держится и волокна g i сами образуют SupIndep, то ∑-образ σ (s.sigma g) сохраняет SupIndep для f.
LaTeX
$$((hs : s.SupIndep (fun i => (g i).sup fun b => f ⟨i, b⟩)) ∧ (hg : ∀ i ∈ s, (g i).SupIndep fun b => f ⟨i, b⟩)) → (s.sigma g).SupIndep f$$
Lean4
/-- Bind operation for `SupIndep`. -/
protected theorem sup [DecidableEq ι] {s : Finset ι'} {g : ι' → Finset ι} {f : ι → α}
(hs : s.SupIndep fun i => (g i).sup f) (hg : ∀ i' ∈ s, (g i').SupIndep f) : (s.sup g).SupIndep f :=
by
simp_rw [supIndep_iff_pairwiseDisjoint] at hs hg ⊢
rw [sup_eq_biUnion, coe_biUnion]
exact hs.biUnion_finset hg
