OAI/GroupTheory/FiniteType/SingularSubdivisionIterateApplyComm.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SingularSubdivision.iterate_apply_comm line 13
  2. lemma OAI.SingularSubdivision.cycle_difference line 17
  3. lemma OAI.SmallChains.d_val line 37
  4. abbrev OAI.SmallChains.scInclusion line 41
  5. lemma OAI.SmallChains.scInclusion_surjective line 44
  6. lemma OAI.SmallChains.scInclusion_injective line 57
  7. theorem OAI.SmallChains.inclusion_quasiIsoAt line 79
  8. theorem OAI.SmallChains.inclusion_quasiIso line 91
  9. def OAI.SingularSupport.cut line 103
  10. lemma OAI.SingularSupport.cut_gen line 106
  11. lemma OAI.SingularSupport.cut_mem line 112
  12. lemma OAI.SingularSupport.cut_eq line 121
  13. lemma OAI.SingularSupport.cut_mem_and line 129
  14. lemma OAI.SingularSupport.span_and line 138
  15. lemma OAI.SingularSupport.span_or line 145
  16. def OAI.SingularSubspace.inclusionMap line 161
  17. abbrev OAI.SingularSubspace.Within line 163
  18. def OAI.SingularSubspace.group line 165
  19. lemma OAI.SingularSubspace.group_inf line 167
  20. def OAI.SingularSubspace.liftSimplex line 172
  21. lemma OAI.SingularSubspace.inclusion_lift line 175
  22. lemma OAI.SingularSubspace.within_inclusion line 178
  23. lemma OAI.SingularSubspace.lift_inclusion line 182
  24. def OAI.SingularSubspace.lift line 185
  25. lemma OAI.SingularSubspace.generator_lift line 188
  26. lemma OAI.SingularSubspace.inclusion_liftChain line 192
  27. lemma OAI.SingularSubspace.liftChain_inclusion line 197
  28. lemma OAI.SingularSubspace.inclusion_injective line 205
  29. lemma OAI.SingularSubspace.inclusion_mem line 211
  30. lemma OAI.SingularSubspace.group_eq_range line 218