module module

`IndisputableMonolith.Foundation.SingularSubdivision`

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 (2)

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

IndisputableMonolith.Foundation.SingularMayerVietoris module_import
IndisputableMonolith.Foundation.SingularSphere module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.SingularPrism module_import

declarations in this module (114)

abbrev AC L93
def asimplex L96
lemma lift_asimplex L109
def abnd L116
lemma abnd_asimplex L122
def acone L129
lemma acone_asimplex L133
def eps L138
lemma eps_asimplex L141
lemma cons_comp_succAbove_zero L147
lemma cons_comp_succAbove_succ L153
theorem abnd_comp_acone L164
theorem abnd_comp_acone_zero L179
theorem abnd_comp_abnd L201
theorem eps_comp_abnd L285
def asub L301
lemma asub_zero L308
lemma asub_asimplex L311
theorem abnd_comp_asub L318
def atee L353
lemma atee_zero L360
lemma atee_asimplex L363
theorem abnd_comp_atee_zero L371
theorem abnd_comp_atee L377
def asubIter L415
lemma asubIter_zero L421
lemma asubIter_succ L424
theorem abnd_comp_asubIter L428
def ateeIter L440
lemma ateeIter_zero L446
lemma ateeIter_succ L449
lemma asubIter_comp_asub L454
theorem abnd_comp_ateeIter L463
def amap L506
lemma amap_asimplex L509
lemma amap_comp_abnd L514
lemma amap_comp_acone L524
theorem amap_comp_asub L538
theorem amap_comp_atee L564
def affineMapFun L602
lemma affineMapFun_mem L606
lemma continuous_affineMapFun L622
def affineMap L630
lemma affineMap_apply_coe L635
lemma affineMap_vertex L640
theorem affineMap_comp L656
def idTuple L667
lemma affineMap_idTuple L671
lemma affineMap_comp_idTuple L686
lemma stdSimplex_map_eq_affineMap L692
lemma affineMap_comp_face L709
def sbary L723
lemma sbary_apply L741
lemma sbary_affineMap L747
def postComp L776
def simplexEquiv L785
lemma simplexEquiv_ L790
lemma simplexEquiv_map L796
def pushSimplex L803
lemma simplexEquiv_pushSimplex L807
def toChain L814
lemma toChain_asimplex L818
lemma pushSimplex_idTuple L833
lemma toChain_asimplex_idTuple L838
lemma toChain_comp_abnd L853
lemma toChain_comp_chainMap L863
lemma toChain_amap L875
def baryFn L888
def sdGen L893
def sdOp L898
lemma gen_sdOp L901
def tGen L905
def tOp L910
lemma gen_tOp L913
lemma gen_pushSimplex_comp_sdOp L918
lemma gen_pushSimplex_comp_tOp L936
theorem sdOp_comp_bnd L954
theorem sdOp_zero L978
theorem tOp_zero L988
theorem tOp_chain_homotopy_succ L998

… and 34 more