piFinset_image — Mathlib

English

The piFinset of images equals the image of the piFinset under the coordinatewise map.

Русский

образ пиFinset равен образу пиFinset под координатной картой.

LaTeX

$$$\\operatorname{piFinset}(\\lambda a. (s(a)).\\mathrm{image}(f(a))) = \\operatorname{piFinset}(s)\\mathrm{.image}(\\lambda b a. f(a)\\, b).$$$

Lean4

theorem piFinset_image [∀ a, DecidableEq (δ a)] (f : ∀ a, γ a → δ a) (s : ∀ a, Finset (γ a)) :
    piFinset (fun a ↦ (s a).image (f a)) = (piFinset s).image fun b a ↦ f _ (b a) := by ext;
  simp only [mem_piFinset, mem_image, Classical.skolem, forall_and, funext_iff]

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