Formalization of Separable Version of Banach–Alaoglu Theorem

Summary In this article, we first formalize the weak sequential compactness in dual normed spaces; then we prove the separable version of Banach– Alaoglu theorem.

Authors

Institutions

Publication Details

Journal
Formalized Mathematics
Published
2025-09-01
DOI
https://doi.org/10.2478/forma-2025-0018
Primary Topic
Nonlinear Differential Equations Analysis
Type
article
Field-Weighted Citation Impact
0.00
Controls
|||
ALL TIME
JAN
FEB
MAR
APR
MAY
JUN
JUL
AUG
SEP
OCT
article

Formalization of Separable Version of Banach–Alaoglu Theorem

Takehiko Mieno, Hiroyuki Okazaki
Formalized Mathematics
Nonlinear Differential Equations Analysis
article

Formalization of Separable Version of Banach–Alaoglu Theorem

Takehiko Mieno, Hiroyuki Okazaki
article en

Abstract

Summary In this article, we first formalize the weak sequential compactness in dual normed spaces; then we prove the separable version of Banach– Alaoglu theorem.

Formalized MathematicsVol. 33(1)
Shinshu University (JP), Epson Information Technology College (JP)
Reduced inequalities
Openalex Percentile: Top 20%
Nonlinear Differential Equations Analysis
DOIOpen Access PDFOpenAlex
AI Navigator

Ask Laika to Summarize, Analyze, and Connect papers live on the map.

Summarize Papers & Methodologies

Extract key findings, datasets, and comparative methods across publications.

Benchmark Rankings & Visual Analytics

Rank top research institutions, authors, funders, topics, and journals by Field-Weighted Citation Impact (FWCI) and paper volume with instant charts.

Connect Distant Disciplines

Bridge topological clusters on the map to find hidden collaborative intersections.

Formalization of Separable Version of Banach–Alaoglu Theorem — Takehiko Mieno, Hiroyuki Okazaki · Formalized Mathematics (2025) | TGRS Research Map | TGRS