OAI/Analysis/JiangSu/DimensionDrop/DimensionDropFibres.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DimensionDropRelations.Witness.mass_E line 22
  2. lemma OAI.DimensionDropRelations.Witness.parameter_E line 23
  3. lemma OAI.DimensionDropRelations.Witness.parameter_column line 24
  4. lemma OAI.DimensionDropRelations.Witness.fibre_h_E line 30
  5. lemma OAI.DimensionDropRelations.Witness.fibre_E_sq line 32
  6. lemma OAI.DimensionDropRelations.Witness.fibre_column_E line 34
  7. def OAI.DimensionDropRelations.Witness.fibreAnchor line 39
  8. def OAI.DimensionDropRelations.Witness.fibreColumn line 40
  9. def OAI.DimensionDropRelations.Witness.fibreEntry line 41
  10. lemma OAI.DimensionDropRelations.Witness.fibreAnchor_star line 46
  11. lemma OAI.DimensionDropRelations.Witness.fibreAnchor_projection line 48
  12. lemma OAI.DimensionDropRelations.Witness.fibreColumn_inner line 56
  13. lemma OAI.DimensionDropRelations.Witness.fibreAnchor_column line 65
  14. lemma OAI.DimensionDropRelations.Witness.fibreColumn_star_anchor line 68
  15. def OAI.DimensionDropRelations.Witness.fibreRow line 72
  16. lemma OAI.DimensionDropRelations.Witness.fibreRow_range line 89
  17. lemma OAI.DimensionDropRelations.Witness.fibreAnchor_commute line 121
  18. lemma OAI.DimensionDropRelations.Witness.h_fibreAnchor line 127
  19. def OAI.DimensionDropRelations.Witness.fibreInner line 131
  20. lemma OAI.DimensionDropRelations.Witness.fibreInner_left line 133
  21. lemma OAI.DimensionDropRelations.Witness.fibreInner_mul line 138
  22. lemma OAI.DimensionDropRelations.Witness.fibreInner_star line 156
  23. lemma OAI.DimensionDropRelations.Witness.fibreInner_sum line 160
  24. def OAI.DimensionDropRelations.Witness.interiorUnits line 164
  25. def OAI.DimensionDropRelations.Witness.interiorHom line 183