iUnion_nonempty_index — Mathlib

English

Let s be a nonempty set and t a function assigning sets to nonempty witnesses; then the union over h of t(h) equals the union over x∈s of t⟨x, proof⟩.

Русский

Пусть s непусто и t — отображение, задающее множества заданным свидетелям; тогда объединение по h: t(h) равно объединению по x∈s: t⟨x, доказательство⟩.

LaTeX

$$$$\\bigcup_{h} t(h) = \\bigcup_{x \\in s} t\\langle x, \\text{proof}(x)\\rangle$$$$

Lean4

theorem iUnion_nonempty_index (s : Set α) (t : s.Nonempty → Set β) : ⋃ h, t h = ⋃ x ∈ s, t ⟨x, ‹_›⟩ :=
  iSup_exists

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