module module

`IndisputableMonolith.Foundation.SingularPrism`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Foundation.SingularMayerVietoris module_import
IndisputableMonolith.Foundation.SingularPair module_import
IndisputableMonolith.Foundation.SingularSphere module_import
IndisputableMonolith.Foundation.SingularSubdivision module_import

declarations in this module (49)

lemma coe_succAbove L43
lemma coe_predAbove L52
def prismSndFun L67
lemma prismSndFun_nonneg L70
lemma prismSndFun_le_one L74
lemma prismSndFun_mem_unitInterval L81
lemma continuous_prismSndFun L85
def prism L93
lemma prism_apply_fst L101
lemma prism_apply_snd L104
def face L110
lemma face_apply L114
lemma map_map_eq_map_map L133
lemma map_map_eq_self L142
lemma sum_filter_map_apply L149
lemma prismSndFun_map_succAbove L157
theorem prism_comp_face_top L164
theorem prism_comp_face_bot L185
theorem prism_comp_face_cancel L212
theorem prism_comp_face_of_le L236
theorem prism_comp_face_of_gt L262
abbrev Idx L294
abbrev Cgrp L298
abbrev gen L303
def prismSimplex L310
def Pgen L319
def prismOp L327
lemma toSSetObjEquiv_ L345
lemma toSSetObjEquiv_map L353
abbrev SC L362
abbrev SOb L367
lemma SC_eq L371
abbrev bnd L375
abbrev chainMap L380
lemma gen_d L386
lemma gen_map L401
lemma gen_prismOp L409
lemma sum_sub_telescope L428
lemma sum_prod_partition L447
lemma sum_prod_partition' L496
lemma prism_sum_cancellation L514
lemma prism_chain_homotopy_succ L760
lemma prism_chain_homotopy_zero L808
abbrev sChainMap L832
def prismHomotopy L838
theorem homotopic_maps_induce_same_homology L876
def chainHomotopyEquiv L887
def homotopyEquiv_homology_iso L904
theorem isIso_homology_map_of_homotopyEquiv L914