OAI/Analysis/JiangSu/DimensionDrop/DimensionDropFibreGenerators.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ConcreteMatrixUnits.System.hom_unit line 15
  2. lemma OAI.DimensionDropRelations.Witness.phi_fibre_split line 28
  3. lemma OAI.DimensionDropRelations.Witness.s_fibre_split line 49
  4. lemma OAI.DimensionDropRelations.Witness.h_eq_one_of_parameter_one line 73
  5. lemma OAI.DimensionDropRelations.Witness.s_eq_zero_of_parameter_one line 78
  6. def OAI.DimensionDropRelations.Witness.upperEndpointHom line 82
  7. lemma OAI.DimensionDropRelations.Witness.zero_fibre_phi_matrix line 91
  8. def OAI.DimensionDropRelations.Witness.lowerEndpointHom line 112
  9. def OAI.DimensionDropModel.amplify line 131
  10. lemma OAI.DimensionDropModel.amplify_apply line 149
  11. lemma OAI.DimensionDropModel.amplify_injective line 151
  12. lemma OAI.DimensionDropModel.amplify_norm line 157
  13. def OAI.DimensionDropModel.flipInner line 160
  14. def OAI.DimensionDropModel.upperEmbed line 165
  15. lemma OAI.DimensionDropModel.upperEmbed_apply line 168
  16. lemma OAI.DimensionDropModel.upperEmbed_norm line 171
  17. abbrev OAI.DimensionDropModel.Mat line 178
  18. def OAI.DimensionDropModel.phi line 179
  19. def OAI.DimensionDropModel.s line 181
  20. lemma OAI.DimensionDropModel.amplify_unit line 183
  21. lemma OAI.DimensionDropModel.phi_zero line 187
  22. lemma OAI.DimensionDropModel.s_zero line 189
  23. lemma OAI.DimensionDropModel.phi_one line 191
  24. lemma OAI.DimensionDropModel.s_one line 198
  25. lemma OAI.DimensionDropRelations.Witness.interiorHom_phi line 211
  26. lemma OAI.DimensionDropRelations.Witness.interiorHom_s line 224