IndisputableMonolith.Foundation.SingularSphere

declarations in this module (55)

• abbrev Hgrp L114
• abbrev Zsingle L118
• def v0 L122
• def pointOf L141
• def constSimplex L145
• lemma pointOf_constSimplex L148
• lemma idx0_ext L155
• lemma constSimplex_pointOf L162
• lemma pointOf_map L167
• lemma pointOf_ L174
• def augFun L184
• lemma gen_augFun L189
• lemma augFun_genUnit L195
• lemma mem_iff_of_clopen_ L204
• lemma bnd_augFun L231
• def augTo L252
• lemma augTo_f_zero L260
• def ptFrom L268
• lemma ptFrom_f_zero L273
• lemma ptFrom_augTo L280
• abbrev ZsingleH0Iso L293
• def augH L297
• def ptH L302
• lemma ptH_augH L308
• lemma id_int_ne_zero L322
• def simplexToI L332
• def pathSimplex L336
• lemma coord_face_v0 L340
• lemma simplexToI_face_v0 L384
• lemma gen_pathSimplex_bnd L409
• lemma subApp L420
• lemma bnd_genUnit_pathSimplex L425
• lemma exists_bnd_eq_sub L436
• lemma exists_bnd_of_pathConnected L447
• lemma augTo_f_zero_apply L477
• lemma Zsingle_d_one_zero L483
• theorem isIso_homologyMap_augTo L490
• theorem isIso_augH_of_pathConnected L511
• lemma isZero_homology_of_totallyDisconnected L524
• theorem isZero_homology_of_contractible L532
• lemma sChainMap_augTo L544
• lemma homologyMap_augH L557
• lemma ptFrom_sChainMap L563
• lemma ptH_natural L573
• def ptFromHomotopy L581
• lemma ptH_eq_of_joined L616
• def h0_iso_int L625
• def h0_pt_iso_int L631
• lemma hn_pt_isZero L636
• def h0_contractible_iso_int L640
• theorem isIso_mv L653
• theorem isZero_of_isZero_inter L682
• theorem mono_mvPair_zero L692
• theorem isZero_h1 L717
• theorem isZero_h1_of_contractible L732