iUnion_decode₂ — Mathlib

English

For f: β → Set α, the union over i ∈ ℕ and b ∈ decode₂ β i of f(b) equals the union over all b ∈ β of f(b): ⋃ (i) (b ∈ decode₂ β i), f(b) = ⋃ b, f(b).

Русский

Для любой функции f: β → множество α объединение по i и b ∈ decode₂ β i множества f(b) равно объединению по всем b ∈ β: ⋃ (i) (b ∈ decode₂ β i), f(b) = ⋃ b, f(b).

LaTeX

$$$ \\bigcup_{i \\in \\mathbb{N}} \\bigcup_{b \\in decode_2(\\beta,i)} f(b) = \\bigcup_{b \\in \\beta} f(b). $$$

Lean4

theorem iUnion_decode₂ (f : β → Set α) : ⋃ (i : ℕ) (b ∈ decode₂ β i), f b = ⋃ b, f b :=
  iSup_decode₂ f

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