English
If every b ≠ a has t(b) nonempty, then the set of values f(a) as f ranges over piFinset t is exactly t(a).
Русский
Если для всех b ≠ a множество t(b) непустое, то множество значений f(a) при f ∈ piFinset t равно t(a).
LaTeX
$$$\\forall a,\\ [\\forall b\\ (b \\neq a \\Rightarrow (t(b)).Nonempty)] \\Rightarrow \\{ f(a) : f \\in \\operatorname{piFinset} t \\} = t(a).$$$
Lean4
theorem eval_image_piFinset (t : ∀ a, Finset (δ a)) (a : α) [DecidableEq (δ a)] (ht : ∀ b, a ≠ b → (t b).Nonempty) :
((piFinset t).image fun f ↦ f a) = t a :=
by
refine (eval_image_piFinset_subset _ _).antisymm fun x h ↦ mem_image.2 ?_
choose f hf using ht
exact ⟨fun b ↦ if h : a = b then h ▸ x else f _ h, by aesop, by simp⟩
