A certified proof of the Cartan fixed point theorems

DOI10.1007/S10817-010-9198-6zbMATH Open1250.68233OpenAlexW2135745323MaRDI QIDQ438546FDOQ438546

Authors: Gianni Ciolli, Graziano Gentili, Marco Maggesi 

Publication date: 31 July 2012

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-010-9198-6

Recommendations

• The HOL Light theory of Euclidean space
• Theorem Proving in Higher Order Logics
• A formalization of metric spaces in HOL Light
• A generalization of Cartan's theorem to proper holomorphic mappings
• Remarks to Cartan's second main theorem for holomorphic curves into \(\mathbb {P}^N(\mathbb {C})\)

zbMATH Keywords

formal proofcomplex analysisCartan fixed point theoremsHOL-light

Mathematics Subject Classification ID

Maximum principle, Schwarz's lemma, Lindelöf principle, analogues and generalizations; subordination (30C80) Holomorphic functions of several complex variables (32A99)

Cites Work

• Rigidity of Holomorphic Mappings and a New Schwarz Lemma at the Boundary
• Title not available (Why is that?)
• Quaternionic analysis
• A new theory of regular functions of a quaternionic variable
• A new approach to Cullen-regular functions of a quaternionic variable
• Title not available (Why is that?)
• A Declarative Language for the Coq Proof Assistant
• Title not available (Why is that?)
• Formal proof - the four color theorem
• Die Funktionentheorie der Differentialgleichungen \(\Delta u=0\) und \(\Delta\Delta u=0\) mit vier reellen Variablen
• Power series and analyticity over the quaternions
• Theorem Proving in Higher Order Logics
• Extension results for slice regular functions of a quaternionic variable
• Sur les fonctions de plusieurs variables complexes. L'itération des transformations intérieures d'un domaine borné
• Reelle Transformationsgruppen und invariante Metriken auf komplexen Räumen
• Title not available (Why is that?)
• Recent Developments for Regular Functions of a Hypercomplex Variable
• Formal proof
• Formal proof -- theory and practice
• Title not available (Why is that?)

Cited In (2)

• Formalizing basic quaternionic analysis
• The HOL Light theory of Euclidean space

Uses Software

• Coq
• Isabelle/Isar
• HOL Light

This page was built for publication: A certified proof of the Cartan fixed point theorems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q438546)