English
Let f_i : α_i → β_i be a family of maps indexed by ι, and let s ⊆ ι with t_i ⊆ α_i for each i. If f_i is surjective for every i not in s, then the image of the product map Pi.map f on the dependent product s ⊓ t equals the dependent product over i of the images f_i''t_i; i.e. the image of the map on s.pi t is exactly s.pi (i ↦ f_i''t_i).
Русский
Пусть для каждого i∈ι дано отображение f_i : α_i → β_i, и пусть s ⊆ ι, а для каждого i задано t_i ⊆ α_i. Если для всех i ∉ s отображение f_i сюръективно, то образ произведения Pi.map f над зависимым произведением s.pi t равен зависимому произведению образов f_i''t_i: image(Pi.map f)(s.pi t) = s.pi (i ↦ f_i''t_i).
LaTeX
$$$$ \\operatorname{image}(\\Pi f)(s \\pi t) = s \\pi \\bigl(i \\mapsto f_i'' t_i\\bigr). $$$$
Lean4
theorem piMap_image_pi {f : ∀ i, α i → β i} (hf : ∀ i ∉ s, Surjective (f i)) (t : ∀ i, Set (α i)) :
Pi.map f '' s.pi t = s.pi fun i ↦ f i '' t i :=
by
refine Subset.antisymm (piMap_image_pi_subset _) fun b hb => ?_
have (i : ι) : ∃ a, f i a = b i ∧ (i ∈ s → a ∈ t i) := by
if hi : i ∈ s then exact (hb i hi).imp fun a ⟨hat, hab⟩ ↦ ⟨hab, fun _ ↦ hat⟩
else exact (hf i hi (b i)).imp fun a ha ↦ ⟨ha, (absurd · hi)⟩
choose a hab hat using this
exact ⟨a, hat, funext hab⟩
