Summable family in a commutative group

DOI10.1515/FORMA-2015-0022zbMath1334.54005OpenAlexW2328655190MaRDI QIDQ271890

Roland Coghetto

Publication date: 20 April 2016

Published in: Formalized Mathematics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1515/forma-2015-0022

zbMATH Keywords

topological grouplimitsfiltersconvergence serieslinear topological spacesummable family

Mathematics Subject Classification ID

Structure of general topological groups (22A05) Topological groups (topological aspects) (54H11) Mechanization of proofs and logical operations (03B35) Convergence in general topology (sequences, filters, limits, convergence spaces, nets, etc.) (54A20)

Related Items (1)

Double sequences and iterated limits in regular space

Uses Software

• Isabelle/HOL
• Mizar

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Groups -- additive notation.
• Convergent filter bases
• Formalization of real analysis: a survey of proof assistants and libraries
• Mizar: State-of-the-art and Beyond
• Type Classes and Filters for Mathematical Analysis in Isabelle/HOL

This page was built for publication: Summable family in a commutative group