English
For a finitely supported function l on a dependent sum, the support of l is exactly the sigma of the supports of each split component.
Русский
Для функции с конечной опорой на зависимую сумму множество опор функции l совпадает с объединением по сигма-разбиению опор её компонент.
LaTeX
$$$\\\\operatorname{supp}(l) =\\\\,\\\\operatorname{splitSupport}(l)\\\\.\\\\sigma(\\\\lambda i, (l\\\\.split i).\\\\operatorname{support})$$$
Lean4
theorem sigma_support : l.support = l.splitSupport.sigma fun i => (l.split i).support :=
by
simp_rw [Finset.ext_iff, splitSupport, split, comapDomain, Sigma.forall, mem_sigma, mem_image, mem_preimage]
tauto