insert_pi — Mathlib

English

The pi-set over an index set with an inserted element i equals the intersection of the preimage of t i at i and the pi-set over the original s.

Русский

Пусть i вставлен в множество индексов; тогда π над insert i s равен пересечению преизображения t i по i и π s t.

LaTeX

$$$ \pi(\mathrm{insert}\ i\ s)\ t = (\mathrm{eval}\ i)^{-1}'(t_i) \cap (\pi s t) $$$

Lean4

@[simp]
theorem insert_pi (i : ι) (s : Set ι) (t : ∀ i, Set (α i)) : pi (insert i s) t = eval i ⁻¹' t i ∩ pi s t := by grind

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