univ_pi_piecewise — Mathlib

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]

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