Finiteness of support #
theorem
Function.mulSupport_along_fiber_finite_of_finite
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[One γ]
(f : Prod α β → γ)
(a : α)
(h : (mulSupport f).Finite)
:
(mulSupport fun (b : β) => f { fst := a, snd := b }).Finite