OAI/Analysis/CircleDomains/Topology/EntireHomeomorphAffine.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

An entire plane homeomorphism is affine. Its analytic infinity germ supplies principal normalization, after which Liouville applies to the entire remainder.

  1. lemma OAI.CircleDomainRigidity.entire_homeomorph_affine line 13