IndisputableMonolith.Foundation.LinkingVanishingHighDim

declarations in this module (43)

• def linkingComplementH1 L69
• def DetectsNontrivialLinking L76
• def ArcComplementsAcyclic L88
• def pt2 L96
• lemma pt2_zero L99
• lemma pt2_one L101
• lemma pt2_norm L103
• lemma pt2_mem_sphere L109
• lemma coord_sq_add_sq L114
• lemma sq_coord0_le_one L120
• def arcFun L125
• lemma arcFun_coord0 L135
• lemma arcFun_coord1 L138
• lemma continuous_arcFun L141
• def arcMap L155
• lemma arcMap_injective L159
• lemma isEmbedding_arcMap L167
• def arcPlus L175
• def arcMinus L179
• lemma isEmbedding_arcPlus L182
• lemma isEmbedding_arcMinus L185
• def arcParam L189
• lemma arcFun_arcParam L199
• lemma range_arcPlus L218
• lemma range_arcMinus L231
• lemma range_arcPlus_union_arcMinus L245
• lemma range_arcPlus_inter_arcMinus L253
• lemma eastP_ne_westP L301
• def perpIsometry L312
• lemma stereographic_source_pt L320
• def twoPunctHomeo L329
• def punctTranslateHomeo L385
• def twoPointComplHEquiv L396
• theorem isZero_h2_twoPointCompl L408
• theorem isZero_h1_inter L420
• def flattenComplHomeo L434
• theorem isZero_h1_unionCompl L452
• theorem isZero_h1_complement_of_embedding L518
• def toSphMap L565
• lemma isEmbedding_toSphMap L573
• def complDownHomeo L582
• theorem not_detects_of_arcAcyclic L603
• theorem forces_D3_of_arcAcyclic L615