IndisputableMonolith.Foundation.SingularMayerVietoris

declarations in this module (147)

• def Small L90
• def SIdx L108
• abbrev sCgrp L112
• def sgen L116
• def sInc L121
• lemma sgen_sInc L124
• def sRet L131
• lemma sInc_comp_sRet L135
• lemma sInc_mono L146
• def sBnd L151
• lemma sgen_sBnd L155
• lemma sBnd_comp_sInc L161
• lemma sBnd_comp_sBnd L175
• def SSC L185
• lemma SSC_X L188
• lemma SSC_d L190
• def small L195
• lemma small L202
• lemma mapSmul L215
• lemma zeroApp L219
• def ev1 L225
• lemma ev1_apply L230
• def unitOf L237
• lemma comp_unitOf L240
• lemma span_unitOf_eq_top L247
• lemma freeInduction L279
• def genUnit L299
• lemma genUnit_eq L302
• def smallSpan L306
• lemma genUnit_mem_smallSpan L309
• def sUnit L315
• lemma sInc_sUnit L318
• lemma sInc_injective L328
• lemma sInc_mem_smallSpan L337
• lemma exists_sInc_eq L349
• lemma toChain_one_mem_smallSpan L362
• lemma small_pushSimplex L373
• lemma sdOp_mem_smallSpan L385
• lemma tOp_mem_smallSpan L401
• lemma sdOpIter_mem_smallSpan L416
• lemma tOpIter_mem_smallSpan L426
• lemma sdOpIter_add L444
• lemma exists_sdOpIter_mem_smallSpan L454
• lemma sub_sdOpIter_eq_bnd_succ L484
• lemma sub_sdOpIter_eq_bnd_zero L502
• lemma sdOpIter_bnd_elem L515
• lemma sub_sdOpIter_eq_bnd_of_boundary L523
• def kerMap L558
• lemma kerMap_coe L562
• lemma kerMap_range_le L565
• def quotMap L576
• def lhMapData L583
• lemma quotMap_surjective L601
• lemma quotMap_injective L619
• lemma isIso_homologyMap_of_elementwise L646
• lemma epi_homologyMap_of_elementwise L664
• lemma isIso_homologyMap_of_sc' L683
• lemma epi_homologyMap_of_sc' L710
• lemma isIso_homologyMap_chain_succ L736
• lemma isIso_homologyMap_chain_zero L749
• lemma epi_homologyMap_chain_zero L769
• lemma small_surj_succ L793
• lemma small_inj L813
• theorem small L840
• def smallChainsHomologyIso L884
• def coordAt L900
• lemma coordAt_unitOf L903
• lemma coordAt_zero L913
• lemma coordAt_add L919
• lemma coordAt_smul L925
• def suppOf L932
• lemma mem_suppOf_iff L935
• lemma sum_coordAt_smul_unitOf L942
• lemma coordAt_map_eq L971
• lemma coordAt_map_notMem L986
• lemma addApp L1007
• lemma negApp L1013
• lemma biprod_decomp L1021
• lemma biprod_elem_ext L1036
• lemma descApp L1043

… and 67 more