Finiteness of support

@[simp]

theorem Function.mulSupport_along_fiber_finite_of_finite {α : Type u_1} {β : Type u_2} {γ : Type u_3} [One γ] (f : α × β → γ) (a : α) (h : (mulSupport f).Finite) : (mulSupport fun (b : β) => f (a, b)).Finite

@[simp]

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