如何证明Coq中既不是内射也不是满射的常数函数？
相关标签：
因此，定义如下：Definition constant {X:Type} (c:X) := fun x y : X => y = c.我需要证明Theorem const_not_inj : forall c:nat, ~injective (constant c).
我开始这样证明：
Theorem const_not_inj : forall c:nat, ~injective (constant c).
unfold injective.
unfold not.
intros.
induction c.
然后我就被困住了，不知道如何继续下去。任何想法都会有帮助：）
特别声明：以上内容（图片及文字）均为互联网收集或者用户上传发布，本站仅提供信息存储服务！如有侵权或有涉及法律问题请联系我们。
举报
