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 : HasFiniteMulSupport f)
:
HasFiniteMulSupport fun (b : β) => f (a, b)
@[simp]
theorem
Function.support_along_fiber_finite_of_finite
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Zero γ]
(f : α × β → γ)
(a : α)
(h : HasFiniteSupport f)
:
HasFiniteSupport fun (b : β) => f (a, b)