OAI/Geometry/BallPacking/Fredholm/CompactFredholmAlternative.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.HigherDimensionalBallPacking.Rigidity.compactPerturbation_surjective_of_injective line 14
  2. theorem OAI.HigherDimensionalBallPacking.Rigidity.compactPerturbation_injective_iff_surjective line 33
  3. def OAI.ContinuousLinearMap.FredholmPackage.domCoords line 47
  4. def OAI.ContinuousLinearMap.FredholmPackage.codCoords line 50
  5. def OAI.ContinuousLinearMap.FredholmPackage.finitePerturbation line 53
  6. theorem OAI.ContinuousLinearMap.FredholmPackage.finitePerturbation_compact line 56
  7. theorem OAI.ContinuousLinearMap.FredholmPackage.finitePerturbation_coords line 64
  8. theorem OAI.ContinuousLinearMap.FredholmPackage.finitePerturbation_injective line 78
  9. theorem OAI.ContinuousLinearMap.FredholmPackage.finitePerturbation_surjective line 96
  10. theorem OAI.HigherDimensionalBallPacking.Rigidity.finrank_eq_of_map_alternative line 126
  11. theorem OAI.HigherDimensionalBallPacking.Rigidity.compactPerturbation_package_finrank line 154
  12. theorem OAI.HigherDimensionalBallPacking.Rigidity.compactPerturbation_index_zero line 167
  13. abbrev OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.complexI line 193
  14. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.principalCR line 195
  15. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.principalCR_value line 199
  16. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedPrincipal line 209
  17. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedPrincipal_value line 220
  18. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.frameCRCoefficient line 225
  19. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.frameCRCoefficient_value line 230
  20. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.frameCRCoefficient_zero_outside line 234
  21. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.coefficientAction_standardCR line 243
  22. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.frame_principal_pointwise line 251
  23. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.frame_conjugates_principal line 265
  24. lemma OAI.HigherDimensionalBallPacking.Rigidity.fredholm_post_equiv line 290
  25. lemma OAI.HigherDimensionalBallPacking.Rigidity.fredholm_pre_equiv line 297
  26. lemma OAI.HigherDimensionalBallPacking.Rigidity.post_equiv_ker line 304
  27. lemma OAI.HigherDimensionalBallPacking.Rigidity.post_equiv_range line 310
  28. lemma OAI.HigherDimensionalBallPacking.Rigidity.post_equiv_finrank_coker line 314
  29. lemma OAI.HigherDimensionalBallPacking.Rigidity.pre_equiv_range line 319
  30. def OAI.HigherDimensionalBallPacking.Rigidity.preEquivKernel line 326
  31. lemma OAI.HigherDimensionalBallPacking.Rigidity.index_zero_post_equiv line 338
  32. lemma OAI.HigherDimensionalBallPacking.Rigidity.index_zero_pre_equiv line 345
  33. lemma OAI.HigherDimensionalBallPacking.Rigidity.equiv_add_compact_fredholm line 352
  34. lemma OAI.HigherDimensionalBallPacking.Rigidity.equiv_add_compact_index_zero line 362
  35. lemma OAI.HigherDimensionalBallPacking.Rigidity.conjugated_normal_form line 373
  36. lemma OAI.HigherDimensionalBallPacking.Rigidity.framed_compact_perturbation_fredholm line 383
  37. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.compact_subset_bump_inner line 404
  38. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.markedZeroOrder_isCompact_of_compact line 412
  39. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.structureAlong_compactPerturbation line 442
  40. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.smoothAlongJet line 450
  41. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.smoothAlongJet_value line 454
  42. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.smoothMarkedPrincipal line 456
  43. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.smoothMarkedPrincipal_value line 459
  44. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.compatible_frame_cr_compact line 463
  45. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.compatible_frame_cr_identity line 469
  46. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.compatibleFrameError line 483
  47. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.compatibleFrameError_compact line 488
  48. def OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.compatiblePrincipalCoords line 491
  49. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.compatiblePrincipalCoords_toCLM line 494
  50. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.compatible_normal_form line 499
  51. lemma OAI.HigherDimensionalBallPacking.Rigidity.HolderCompletion.smoothMarkedPrincipal_add_compact_fredholm line 506