English
For each i, the image of the product filter π f under the projection eval i equals f i: map (eval i) (π f) = f i.
Русский
Образ произведения π f при проекции eval i совпадает с f i: map (eval i) (π f) = f i.
LaTeX
$$$\\operatorname{map}(\\operatorname{eval} i)(\\pi f) = f i$$$
Lean4
@[simp]
theorem map_eval_pi (f : ∀ i, Filter (α i)) [∀ i, NeBot (f i)] (i : ι) : map (eval i) (pi f) = f i :=
by
refine le_antisymm (tendsto_eval_pi f i) fun s hs => ?_
rcases mem_pi.1 (mem_map.1 hs) with ⟨I, hIf, t, htf, hI⟩
rw [← image_subset_iff] at hI
refine mem_of_superset (htf i) ((subset_eval_image_pi ?_ _).trans hI)
exact nonempty_of_mem (pi_mem_pi hIf fun i _ => htf i)
