∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (f g : ModularForm Γ k) {c : OnePoint ℝ},
  IsCusp c Γ → c.IsBoundedAt ({ toFun := ⇑f, slash_action_eq' := ⋯ } + { toFun := ⇑g, slash_action_eq' := ⋯ }).toFun k