论文部分内容阅读
本文给出一种用高阶逻辑自动证明语言Isabelle在计算机中表示拓扑空间中开集、闭集、邻域和导集等基本概念的方法,在此基础上证明点集拓扑学中著名的杨忠道定理,即一拓扑空间的任意单点集的导集为闭集,则其任意子集的导集亦为闭集.
点集拓扑学之杨忠道定理的一个机械化证明
【摘 要】
：
本文给出一种用高阶逻辑自动证明语言Isabelle在计算机中表示拓扑空间中开集、闭集、邻域和导集等基本概念的方法,在此基础上证明点集拓扑学中著名的杨忠道定理,即一拓扑空间的任意单点集的导集为闭集,则其任意子集的导集亦为闭集.
【机 构】
：
上海大学数学系,上海200444;河南大学计算机与信息工程学院,开封475004;华东师范大学上海市高可信计算重点实验室,上海200062;Department of Mathematics, Col
【出 处】
：
中国科学:数学
【发表日期】
：
2021年01期
其他文献
本文提出了一种新型结构的声表面波──二极管卷积器，利用二极管在反向偏置时结电容的非线性，通过声表面波延迟线抽头与二极管直接耦合而获得信号的卷积输出。这种新结构可以更
信息化发展,图书馆服务由物理的实体服务逐渐转入后台的网络化服务.加强古籍、民国文献数字化服务与利用,是解决古籍、民国文献保护与使用矛盾问题的关键.构建IC空间,创设学
永城市审计局最近在商丘市组织的《审计法》实施8周年摄影作品比赛活动中获一等奖,受到商丘市审计局通报表彰。上报的作品反映了审计工作、开展精神文明建设活动等现场照片12
如何设计安全、可靠的信息物理融合系统是计算机科学和控制理论面临的一个重大挑战.时延现象在信息物理融合系统中普遍存在,时延对系统的稳定性、安全性和控制性能具有实质性影响.但是在已有时延系统验证和控制器合成的工作中往往忽略时延因素,这会导致在不考虑时延情况下能保证稳定和安全的系统在实际运行时因为时延原因而不再稳定和安全.因为时延使得系统的行为演化不仅与当前状态有关,还依赖于系统的历史状态,所以时延混成
许多人看望病人时，喜欢送鲜花。看到一簇簇鲜艳夺目、芳香扑鼻的鲜花，病痛缠身的病人不禁心情舒畅许多。在欧美等国家，送花探望病人已经是一种传统，目前在国内也逐渐成为时尚。但据英国《每日电讯报》报道，英国部分医院以危害健康为由，禁止在外科病房摆放鲜花。在我国的成都、长沙等一些城市，也有部分医院禁止将鲜花带入病房。 据有关医学专家介绍，鲜花是一种外源性的致敏原，部分鲜花中含有的花粉，可以作用于人的免疫细
借助于一类张量收缩积,本文定义一类张量空间上的线性互补问题,简称张量线性互补问题.当所涉及的张量变量退化为向量时,所考虑的问题退化为经典的线性互补问题.对此,首先讨论张量收缩积的一些性质,然后建立张量线性互补问题的理论与算法.具体地,讨论张量线性互补问题的等价模型、可行性与可解性理论、解集的凸性等,提出一个求解张量线性互补问题的外梯度算法,在一定条件下证明算法的收敛性,并给出初步的数值实验结果.
资产的联合波动率矩阵是资源配置和风险管理的重要统计量,对其准确估计是金融统计和风险度量中的热点问题之一.本文在带有市场信息的微观结构噪声下,研究带跳对数价格的积分波动率矩阵估计问题.在多资产价格观察不同步下,当资产数和样本量都趋向于无穷时,利用不重叠区间方法和稀疏性特征提出高维积分波动率矩阵的4种估计方法,其收敛速度可以达到已存在高维积分波动率矩阵估计的最优收敛速度.同时,所提出的调整估计量具有相
人体逆向运动学问题是人体运动合成、人体运动捕获和理解的基本问题.由于人体关节链式系统的复杂性,人体逆向运动学方程往往存在多解或无解的情形.传统的方法通常采用解析或数值迭代方法求解逆向运动学问题,在给定足够多约束的情形下能够得到比较好的解,但无法处理少量约束下生成自然的人体姿态问题.近年来,从大规模数据集中学习统计模型参数的思想被广泛运用,求解人体逆向运动学的机器学习方法中经典工作—混合Gauss逆