univ_pi_piecewise_univ — Mathlib

English

When the second component is univ for all indices, the pi-type over univ reduces to pi over s with t.

Русский

Если второе множество для всех индексов равно univ, то pi univ по s.piecewise t univ равно pi s t.

LaTeX

$$$\\pi univ (s.piecewise t (\\lambda i. univ)) = \\pi s t$$$

Lean4

theorem univ_pi_piecewise_univ {ι : Type*} {α : ι → Type*} (s : Set ι) (t : ∀ i, Set (α i)) [∀ x, Decidable (x ∈ s)] :
    pi univ (s.piecewise t fun _ => univ) = pi s t := by simp

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