English
Same as above, with a strengthened existence condition; the image equals t(a).
Русский
То же самое с усиленным условием существования; образ равен t(a).
LaTeX
$$$\\forall a,\\ [\\forall b\\ (b \\neq a \\Rightarrow (t(b)).Nonempty)] \\Rightarrow \\operatorname{image}(\\lambda f. f(a))(\\operatorname{piFinset} t) = t(a).$$$
Lean4
theorem eval_image_piFinset_const {β} [DecidableEq β] (t : Finset β) (a : α) :
((piFinset fun _i : α ↦ t).image fun f ↦ f a) = t :=
by
obtain rfl | ht := t.eq_empty_or_nonempty
· haveI : Nonempty α := ⟨a⟩
simp
· exact eval_image_piFinset (fun _ ↦ t) a fun _ _ ↦ ht