sigma_support — Mathlib

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

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