univ_pi_ite — Mathlib

English

The pi of a universe with coordinatewise ite (i ∈ s) equals the pi over s of t.

Русский

Произведение по всем i уровня с условием ite (i ∈ s) равно произведению по s с t.

LaTeX

$$$$ \\bigl(\\mathrm{pi}\\ \\mathrm{univ}\\ \\lambda i. \\mathrm{ite}(i \\in s, t_i, \\mathrm{univ})\\bigr) = \\mathrm{pi}\\,\\mathrm{univ}\\, t. $$$$

Lean4

theorem univ_pi_ite (s : Set ι) [DecidablePred (· ∈ s)] (t : ∀ i, Set (α i)) :
    (pi univ fun i => if i ∈ s then t i else univ) = s.pi t := by grind

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