IndisputableMonolith.Foundation.SingularSphereGeometry

declarations in this module (66)

• abbrev Esp L89
• def Sph L93
• def northV L97
• lemma norm_northV L100
• def northP L104
• def southP L108
• lemma northP_ne_southP L110
• def coverU L135
• def coverV L138
• lemma isOpen_coverU L140
• lemma isOpen_coverV L142
• lemma coverU_union_coverV L144
• theorem contractibleSpace_compl_singleton_sphere L161
• instance contractible_coverU L176
• instance contractible_coverV L179
• abbrev Hyp L185
• lemma mem_inter_iff L187
• def interHomeoPunctured L198
• def puncturedPolar L255
• def sphereHomeoOfLinearIsometryEquiv L262
• lemma fact_finrank_esp L272
• def hypIsometry L278
• def hequivProdContractible L288
• def interHomotopyEquiv L297
• def hgrpIso L309
• def suspensionIso L316
• abbrev amb L329
• lemma norm_amb L331
• lemma amb_injective L334
• lemma esp0_ext L338
• lemma esp1_ext L346
• lemma northV_ne_zero L354
• lemma abs_eq_one_of_sq_eq_one L357
• lemma amb_southP L366
• lemma sph0_eq_pole L370
• lemma isZero_sph0 L409
• lemma finrank_hyp L414
• lemma one_lt_rank_hyp L419
• instance pathConnected_inter L424
• theorem sphere_homology_vanish L436
• def eastP L459
• def westP L464
• lemma amb_eastP_zero L466
• lemma amb_westP_zero L470
• lemma northV_zero L477
• lemma amb_northP_zero L480
• lemma amb_southP_zero L482
• lemma coord_zero_ne_zero L488
• lemma eastP_mem_inter L520
• lemma westP_mem_inter L533
• abbrev Wc L547
• def aW L551
• def bW L554
• def coordW L557
• def arcA L560
• lemma continuous_coordW L562
• lemma isClopen_arcA L566
• lemma aW_mem_arcA L588
• lemma bW_notMem_arcA L593
• def diffClass L599
• lemma diffClass_pairing L604
• lemma diffClass_mvPair L611
• theorem h1_s1_ne_zero L633
• theorem sphere_top_ne_zero L657
• theorem spheres_not_homotopyEquivalent L671
• theorem sphere_dim_eq_of_homotopyEquiv L686