Registry · Theorem II.T06 established formalized

II.T06 — Holomorphic Implies Continuous

Holomorphic Implies Continuous

Book II Part 2 Ch. 11

Dependency Graph

Depends on (3)

II.L01 II.D10 I.D47

Depended on by (9)

II.D18a II.D72 II.D77 II.R05 II.R06b II.R33 II.T49 II.D91 II.D92

Lean Formalization

Module: TauLib.BookII.Domains.HolImpliesCont

Symbol: hol_cont_check