iUnion_univ_pi_of_monotone — Mathlib

English

A special case with constant domain: union over j of pi of univ is equal to pi of univ of unions.

Русский

Особый случай: объединение по j от pi(univ) равно pi(univ) от объединений.

LaTeX

$$$\bigcup_{j} \text{pi univ } (s(i)) = \text{pi univ } (\bigcup_{j} s(i)).$$$

Lean4

theorem iUnion_univ_pi_of_monotone {ι ι' : Type*} [LinearOrder ι'] [Nonempty ι'] [Finite ι] {α : ι → Type*}
    {s : ∀ i, ι' → Set (α i)} (hs : ∀ i, Monotone (s i)) :
    ⋃ j : ι', pi univ (fun i => s i j) = pi univ fun i => ⋃ j, s i j :=
  iUnion_pi_of_monotone finite_univ fun i _ => hs i

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