English
A variant of the sigma-binding rule for SupIndep: under appropriate conditions on g, the sigma construction preserves SupIndep with respect to f.
Русский
Вариант правила связки сигма для SupIndep: при подходящих условиях на g оператор сигма сохраняет SupIndep относительно f.
LaTeX
$$Theorem sigma: given hs and hg as in the previous variant, (s.sigma g).SupIndep f holds.$$
Lean4
/-- Bind operation for `SupIndep`. -/
protected theorem sigma {β : ι → Type*} {s : Finset ι} {g : ∀ i, Finset (β i)} {f : Sigma β → α}
(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 := by
rintro t ht ⟨i, b⟩ hi hit
rw [Finset.disjoint_sup_right]
rintro ⟨j, c⟩ hj
have hbc := (ne_of_mem_of_not_mem hj hit).symm
replace hj := ht hj
rw [mem_sigma] at hi hj
obtain rfl | hij := eq_or_ne i j
· exact (hg _ hj.1).pairwiseDisjoint hi.2 hj.2 (sigma_mk_injective.ne_iff.1 hbc)
· refine (hs.pairwiseDisjoint hi.1 hj.1 hij).mono ?_ ?_
· convert le_sup (α := α) hi.2; simp
· convert le_sup (α := α) hj.2; simp
