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 : Set.Finite (Function.support f))
:
Set.Finite (Function.support fun (b : β) => f (a, b))
@[simp]
theorem
Function.mulSupport_along_fiber_finite_of_finite
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[One γ]
(f : α × β → γ)
(a : α)
(h : Set.Finite (Function.mulSupport f))
:
Set.Finite (Function.mulSupport fun (b : β) => f (a, b))