有没有办法像rewrite lem in *一样,为所有可能的H调用applylem in H Axiom P Q : nat -> Prop.Axiom lem : forall (n : nat), P n -> Q n.
Goal P O -> P (S O) -> True.intros. applylem in H. applylem in H0.
我试着在Mathematica 8中将三次样条定义为函数,因为我已经得到了每个区间[x_{i}, x_{i + 1}], i = 0, ..., n的每个P_{i} (当然,是3次多项式)。我想要做的是将interval [x_{0}, x_{n + 1}]中的s定义为s(x) = P_{i}(x) if x is in [x_{i}, x_{i+1}]。当n变化时,我如何做到这一点呢?