IndisputableMonolith.Foundation.ArcComplementAcyclic

declarations in this module (60)

• lemma inv_hom_apply L67
• lemma hom_inv_apply L70
• lemma hom_apply_eq_zero_iff L73
• lemma eq_zero_of_isZero L83
• def scIso L103
• def classOf L108
• lemma classOf_eq_zero_iff L116
• lemma exists_classOf L133
• lemma classOf_natural L151
• lemma chainMap_bnd L221
• lemma chainMap_cycle L228
• lemma chainMap_chainMap L233
• lemma chainMap_id L241
• lemma bounds_map L249
• lemma bounds_of_retract L255
• def cls L266
• lemma cls_eq_zero_iff L270
• lemma cls_natural L274
• lemma exists_nonbounding L281
• lemma bounds_of_isZero L296
• def cInc L310
• def cVal L316
• lemma cVal_injective L319
• lemma cInc_comp L322
• lemma cInc_comp_cVal L327
• lemma cInc_cInc_id L332
• def homeoHom L338
• lemma homeoHom_comp_symm L342
• lemma homeoHom_symm_comp L347
• def cPush L355
• lemma range_cPush L359
• def cLift L369
• lemma cPush_cLift L376
• lemma chainMap_cVal_unitOf L385
• lemma exists_chain_lift L393
• theorem bounds_of_mv L427
• def unionComplHomeo L470
• theorem bounds_of_halves L489
• def seg L567
• lemma seg_subset_range L570
• lemma range_subset_seg L573
• lemma seg_mono L577
• lemma isCompact_seg L582
• lemma isClosed_seg L591
• lemma seg_union L596
• lemma seg_inter L612
• def zSeg L633
• def Bad L639
• lemma zSeg_cycle L643
• lemma zSeg_restrict L649
• lemma bad_step L656
• def badSeq L699
• lemma badSeq_zero L711
• lemma badSeq_succ L713
• lemma badSeq_width L721
• lemma badSeq_mono L732
• lemma badSeq_anti L735
• lemma badSeq_le L738
• lemma badSeq_props L748
• theorem arcComplementsAcyclic L761