The Lean 4 theorem `single_mem_mulDomain` in the `ChapterUnboundedPosition` chapter of the timepiece formalization

-- Generated from ChapterUnboundedPosition.lean — theorem BookProof.ChapterUnboundedPosition.single_mem_mulDomain
import Mathlib
import Definitions.Def_ChapterUnboundedPosition
import Definitions.Def_ChapterContinuityUnitaryInfinite
open BookProof.ChapterContinuityUnitaryInfinite
open BookProof.ChapterUnboundedPosition


open scoped ENNReal InnerProductSpace


open BookProof.ChapterContinuityUnitaryInfinite (L2Z)

theorem BookProof.ChapterUnboundedPosition.single_mem_mulDomain (f : ℤ → ℝ) (n : ℤ) (c : ℂ) :
    lp.single 2 n c ∈ mulDomain f := by sorry