pi_piecewise — Mathlib

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 _ _ _

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