pi_univ_ite — Mathlib

English

The pi over univ with a pointwise if-then-else equals the pi with a variable t.

Русский

Пи по универсуму с точечным условием равно пи по функции t (с условием).

LaTeX

$$$ \pi univ (\lambda i. if i \in s then t i else univ) = s.pi t $$$

Lean4

@[simp]
theorem pi_univ_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

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