REPOZYTORIUM UNIWERSYTETU
W BIAŁYMSTOKU
UwB

Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji: http://hdl.handle.net/11320/4897
Tytuł: Weak Convergence and Weak Convergence
Autorzy: Narita, Keiko
Shidama, Yasunari
Endou, Noboru
Słowa kluczowe: normed linear spaces
Banach spaces
duality and reflexivity
weak topologies
weak* topologies
Data wydania: 2015
Data dodania: 16-gru-2016
Wydawca: De Gruyter Open
Źródło: Formalized Mathematics, Volume 23, Issue 3, 231–241
Abstrakt: AbstractIn this article, we deal with weak convergence on sequences in real normed spaces, and weak* convergence on sequences in dual spaces of real normed spaces. In the first section, we proved some topological properties of dual spaces of real normed spaces. We used these theorems for proofs of Section 3. In Section 2, we defined weak convergence and weak* convergence, and proved some properties. By RNS_Real Mizar functor, real normed spaces as real number spaces already defined in the article [18], we regarded sequences of real numbers as sequences of RNS_Real. So we proved the last theorem in this section using the theorem (8) from [25]. In Section 3, we defined weak sequential compactness of real normed spaces. We showed some lemmas for the proof and proved the theorem of weak sequential compactness of reflexive real Banach spaces. We referred to [36], [23], [24] and [3] in the formalization.
Afiliacja: Keiko Narita - Hirosaki-city, Aomori, Japan
Yasunari Shidama - Shinshu University, Nagano, Japan
Noboru Endou - Gifu National College of Technology, Gifu, Japan
Sponsorzy: This work was supported by JSPS KAKENHI 22300285 and 2350002.
URI: http://hdl.handle.net/11320/4897
DOI: 10.1515/forma-2015-0019
ISSN: 1426-2630
1898-9934
Typ Dokumentu: Article
Występuje w kolekcji(ach):Formalized Mathematics, 2015, Volume 23, Issue 3

Pliki w tej pozycji:
Plik Opis RozmiarFormat 
forma-2015-0019.pdf276,14 kBAdobe PDFOtwórz
Pokaż pełny widok rekordu Zobacz statystyki


Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL Creative Commons