Documentation

Mathlib.Algebra.Group.FiniteSupport

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