preimage_pi — Mathlib

English

The preimage of a pi-set under the coordinatewise map g ↦ f_i(g_i) equals the pi-set of the coordinatewise preimages.

Русский

Прообраз π-произведения под отображением g ↦ f_i(g_i) равен π-произведению предобразов.

LaTeX

$$$ (\lambda g i \mapsto f_i(g_i))^{-1}'(\pi t) = \pi (i \mapsto f_i^{-1}'(t_i)) $$$

Lean4

theorem preimage_pi (s : Set ι) (t : ∀ i, Set (β i)) (f : ∀ i, α i → β i) :
    (fun (g : ∀ i, α i) i => f _ (g i)) ⁻¹' s.pi t = s.pi fun i => f i ⁻¹' t i :=
  rfl

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