Evolutionary Quasi-Variational-Hemivariational Inequalities I: Existence and Optimal Control

We study a nonlinear evolutionary quasi–variational–hemivariational inequality (in short, (QVHVI)) involving a set-valued pseudo-monotone map. The central idea of our approach consists of introducing a parametric variational problem that defines a variational selection associated with (QVHVI). We prove the solvability of the parametric variational problem by employing a surjectivity theorem for the sum of operators, combined with Minty’s formulation and techniques from the nonsmooth analysis. Then, an existence theorem for (QVHVI) is established by using Kluge’s fixed point theorem for set-valued operators. As an application, an abstract optimal control problem for the (QVHVI) is investigated. We prove the existence of solutions for the optimal control problem and the weak sequential compactness of the solution set via the Weierstrass minimization theorem and the Kuratowski-type continuity properties.

Formalization of the Equivalence among Completeness Theorems of Real Number in Coq

The formalization of mathematics based on theorem prover becomes increasingly important in mathematics and computer science, and, particularly, formalizing fundamental mathematical theories becomes especially essential. In this paper, we describe the formalization in Coq of eight very representative completeness theorems of real numbers. These theorems include the Dedekind fundamental theorem, Supremum theorem, Monotone convergence theorem, Nested interval theorem, Finite cover theorem, Accumulation point theorem, Sequential compactness theorem, and Cauchy completeness theorem. We formalize the real number theory strictly following Landau’s Foundations of Analysis where the Dedekind fundamental theorem can be proved. We extend this system and complete the related notions and properties for finiteness and sequence. We prove these theorems in turn from Dedekind fundamental theorem, and finally prove the Dedekind fundamental theorem by the Cauchy completeness theorem. The full details of formal proof are checked by the proof assistant Coq, which embodies the characteristics of reliability and interactivity. This work can lay the foundation for many applications, especially in calculus and topology.

Some remarks on bv(s)-metric spaces and fixed point results with an application

We compare the newly defined bv(s)-metric spaces with several other abstract spaces like metric spaces, b-metric spaces and show that some well-known results, which hold in the latter class of spaces, may not hold in bv(s)-metric spaces. Besides, we introduce the notions of sequential compactness and bounded compactness in the framework of bv(s)-metric spaces. Using these notions, we prove some fixed point results involving Nemytzki–Edelstein type mappings in this setting, from which several comparable fixed point results can be deduced. In addition to these, we find some existence and uniqueness criteria for the solution to a certain type of mixed Fredholm–Volterra integral equations.

More on closed non-vanishing ideals in CB(X)

Let X be a completely regular topological space. For each closed non-vanishing ideal H of CB(X), the normed algebra of all bounded continuous scalar-valued mappings on X equipped with pointwise addition and multiplication and the supremum norm, we study its spectrum, denoted by 𝔰𝔭(H). We make a correspondence between algebraic properties of H and topological properties of 𝔰𝔭(H). This continues some previous studies, in which topological properties of 𝔰𝔭(H) such as the Lindelöf property, paracompactness, σ-compactness and countable compactness have been made into correspondence with algebraic properties of H. We study here other compactness properties of 𝔰𝔭(H) such as weak paracompactness, sequential compactness and pseudocompactness. We also study the ideal isomorphisms between two non-vanishing closed ideals of CB(X).

A Note on I-Sequentially Compact Spaces

this paper investigates the properties of convergence and sequentially compact for the generalized concepts –I-convergent and I -sequentially compact. We extend Cartesian product properties of convergence to I-convergence. Further, we develop some properties of -sequential compactness of a topologicalspace.

Compactness in Metric Spaces

Summary In this article, we mainly formalize in Mizar [2] the equivalence among a few compactness definitions of metric spaces, norm spaces, and the real line. In the first section, we formalized general topological properties of metric spaces. We discussed openness and closedness of subsets in metric spaces in terms of convergence of element sequences. In the second section, we firstly formalize the definition of sequentially compact, and then discuss the equivalence of compactness, countable compactness, sequential compactness, and totally boundedness with completeness in metric spaces. In the third section, we discuss compactness in norm spaces. We formalize the equivalence of compactness and sequential compactness in norm space. In the fourth section, we formalize topological properties of the real line in terms of convergence of real number sequences. In the last section, we formalize the equivalence of compactness and sequential compactness in the real line. These formalizations are based on [20], [5], [17], [14], and [4].