OAI/Analysis/CircleDomains/Topology/RealPartBoundaryMaximum.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A boundary maximum principle requiring only upper limits of the real part. The holomorphic function itself need not extend continuously to the boundary. This is used before constructing boundary extensions.

  1. lemma OAI.CircleDomainRigidity.real_part_le_of_boundary_upper_limits line 14