English
The pi-type over univ with a piecewise t t' equals the intersection of pi on s and pi on sᶜ with t and t' accordingly.
Русский
Пи-тип над всеобщим равен объединению пересечения для s и дополнения относительно t и t'.
LaTeX
$$$\\pi\\!\\text{univ} (s.piecewise t t') = \\pi s t \\cup \\pi s^{c} t'$$$
Lean4
theorem univ_pi_piecewise {ι : Type*} {α : ι → Type*} (s : Set ι) (t t' : ∀ i, Set (α i)) [∀ x, Decidable (x ∈ s)] :
pi univ (s.piecewise t t') = pi s t ∩ pi sᶜ t' := by simp [compl_eq_univ_diff]