univ_pi_update_univ — Mathlib

English

A specialized version of universal update: pi univ (update (univ) i s) equals eval i^{-1} s.

Русский

Особый случай обновления над вселенной: π univ (update (univ) i s) = eval_i^{-1}(s).

LaTeX

$$$ \pi \mathrm{univ} (\mathrm{update} (\lambda j, \mathrm{univ}) i s) = \mathrm{eval}_i^{-1}' s $$$

Lean4

theorem univ_pi_update_univ [DecidableEq ι] (i : ι) (s : Set (α i)) :
    pi univ (update (fun j : ι => (univ : Set (α j))) i s) = eval i ⁻¹' s := by
  rw [univ_pi_update i (fun j => (univ : Set (α j))) s fun j t => t, pi_univ, inter_univ, preimage]

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