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