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].
2
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
A bounded closed convex set K in a Banach space X is said to have quasi-normal structure if each bounded closed convex subset H of K for which diam(H) > 0 contains a point u for which ∥u-x∥ < diam(H) for each x ∈ H. It is shown that if the convex sets on the unit sphere in X satisfy this condition (which is much weaker than the assumption that convex sets on the unit sphere are separable), then relative to various weak topologies, the unit ball in X is compact whenever it is countably compact.
In this note we present a result on compactness in certain Banach spaces of vector valued functions. We demonstrate an application of this result to the questions of existence of solutions of nonlinear differential inclusions on a Banach space.
In this note we present a result on compactness in certain Banach spaces of vector valued functions. We demonstrate an application of this result to the questions of existence of solutions of nonlinear differential inclusions on a Banach space.
5
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
Let $N_α$,B and Q_β be the weighted Nevanlinna space, the Bloch space and the Q space, respectively. Note that B and $Q_β$ are Möbius invariant, but $N_α$ is not. We characterize, in function-theoretic terms, when the composition operator $C_ϕ f=f◦ϕ$ induced by an analytic self-map ϕ of the unit disk defines an operator $C_ϕ:N_α→B$, $B→Q_β$, $N_α→Q_β$ which is bounded resp. compact.
6
Dostęp do pełnego tekstu na zewnętrznej witrynie WWW
Given an open set Ω ⊂ Rm and n > 1, we introduce the new spaces GBnV(Ω) of Generalized functions of bounded higher variation and GSBnV(Ω) of Generalized special functions of bounded higher variation that generalize, respectively, the space BnV introduced by Jerrard and Soner in [43] and the corresponding SBnV space studied by De Lellis in [24]. In this class of spaces, which allow as in [43] the description of singularities of codimension n, the distributional jacobian Ju need not have finite mass: roughly speaking, finiteness of mass is not required for the (m−n)-dimensional part of Ju, but only finiteness of size. In the space GSBnV we are able to provide compactness of sublevel sets and lower semicontinuity of Mumford-Shah type functionals, in the same spirit of the codimension 1 theory [5,6].
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.