English
If s is a finite set of indices and g maps s into the index set, then whenever the family (f ∘ g) indexed by s is sup-indep, the pulled-back family f over the image of g is sup-indep.
Русский
Пусть s — конечное множество индексов и пусть g: s → ιigeo. Тогда если семейство (f ∘ g) на s является независимым по SupIndep, то образ семейства {f(j) : j ∈ image g} по f также является SupIndep.
LaTeX
$$$s.SupIndep (f \\circ g) \\Rightarrow (s.image\\ g).SupIndep f$$$
Lean4
protected theorem image [DecidableEq ι] {s : Finset ι'} {g : ι' → ι} (hs : s.SupIndep (f ∘ g)) :
(s.image g).SupIndep f := by
intro t ht i hi hit
rcases subset_image_iff.mp ht with ⟨t, hts, rfl⟩
rcases mem_image.mp hi with ⟨i, his, rfl⟩
rw [sup_image]
exact hs hts his (hit <| mem_image_of_mem _ ·)
