OAI/Analysis/CircleDomains/Topology/EmbeddingComponent.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Transport of a connected component through an embedding, used for the finite chart in the sphere.

  1. lemma OAI.CircleDomainRigidity.embedding_image_connectedComponentIn line 11