English
The pi-type over a piecewise family equals the intersection/product of the corresponding pi-types on the overlapping and complement regions.
Русский
Тип пи над кусочно-заданной семейством эквивалентен пересечению соответствующих пи-типов на пересечении и на разности региона.
LaTeX
$$$\\pi s (s'.piecewise t t') = \\pi (s \\cap s') t \\cap \\pi (s \\setminus s') t'$$$
Lean4
@[simp]
theorem pi_piecewise {ι : Type*} {α : ι → Type*} (s s' : Set ι) (t t' : ∀ i, Set (α i)) [∀ x, Decidable (x ∈ s')] :
pi s (s'.piecewise t t') = pi (s ∩ s') t ∩ pi (s \ s') t' :=
pi_if _ _ _