iUnion_univ_pi — Mathlib

English

The union over x of univ.pi (fun a => t a (x a)) equals univ.pi (fun a => ⋃ j, t a j).

Русский

Объединение по x: ⋃ x, univ.pi (fun a => t(a)(x(a))) равно univ.pi (fun a => ⋃_j t(a)(j)).

LaTeX

$$$$ \bigcup_{x : (a : \alpha) \to \text{Type}} \mathrm{univ}.\pi (\lambda a, t(a)(x(a))) = \mathrm{univ}.\pi (\lambda a, \bigcup_{j} t(a)(j)) $$$$

Lean4

theorem iUnion_univ_pi {ι : α → Type*} (t : (a : α) → ι a → Set (π a)) :
    ⋃ x : (a : α) → ι a, pi univ (fun a => t a (x a)) = pi univ fun a => ⋃ j : ι a, t a j :=
  by
  ext
  simp [Classical.skolem]

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