isPWO_iUnion_support — Mathlib

English

For any summable family, the union of supports across its index set is well-founded (IsPWO).

Русский

Для суммируемой семейства объединение поддержек по индексу образует хорошо упорядоченную коллекцию (IsPWO).

LaTeX

$$$\\text{Set.IsPWO}\\big(\\bigcup_{a\\in\\alpha} (s(a).\\mathrm{support})\\big)$$$

Lean4

theorem isPWO_iUnion_support (s : SummableFamily Γ R α) : Set.IsPWO (⋃ a : α, (s a).support) :=
  s.isPWO_iUnion_support'

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