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

theorem Function.support_along_fiber_finite_of_finite {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Zero γ] (f : Prod α β → γ) (a : α) (h : (support f).Finite) : (support fun (b : β) => f { fst := a, snd := b }).Finite