eval_preimage' — Mathlib

English

Same as above, with a simplified index set {i} instead of univ, i.e. eval preimage for a single coordinate.

Русский

То же самое для множества {i}, т.е. предобраз оценки для одной координаты.

LaTeX

$$$$ \\operatorname{eval}_{i}'^{-1}(s) = \\{\\, \\text{...?} \\,\\} $$$$

Lean4

theorem eval_preimage' [DecidableEq ι] {s : Set (α i)} : eval i ⁻¹' s = pi { i } (update (fun _ => univ) i s) :=
  by
  ext
  simp

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