English
The pi-set over s of a pointwise if-then-else family equals the intersection of pi over s with p and pi over s with not-p.
Русский
Множество π над s для семейства t i, заданного через if p i then t1 i else t2 i, равно пересечению π над s и p и π над s и не-p.
LaTeX
$$$ \pi s (\lambda i, \mathrm{if}\ p_i\ \mathrm{then}\ t_1 i\ \mathrm{else}\ t_2 i) = \pi(\{ i \in s \mid p_i \}) t_1 \cap \pi(\{ i \in s \mid \neg p_i \}) t_2$$$
Lean4
theorem pi_if {p : ι → Prop} [h : DecidablePred p] (s : Set ι) (t₁ t₂ : ∀ i, Set (α i)) :
(pi s fun i => if p i then t₁ i else t₂ i) = pi ({i ∈ s | p i}) t₁ ∩ pi ({i ∈ s | ¬p i}) t₂ :=
by
ext f
refine ⟨fun h => ?_, ?_⟩
·
constructor <;>
· rintro i ⟨his, hpi⟩
simpa [*] using h i
· rintro ⟨ht₁, ht₂⟩ i his
by_cases p i <;> simp_all
