OAI/Analysis/JiangSu/DimensionDrop/DimensionDropSquareTransfer.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.JiangSuConstruction.hom_conjugation_difference_bound line 18
  2. theorem OAI.JiangSuConstruction.tensor_connected_half_flip_of_matching line 30
  3. theorem OAI.SequentialCStar.System.finite_set_common_stage line 58
  4. def OAI.SequentialCStar.System.ApproximateConjugacy line 72
  5. def OAI.SequentialCStar.System.FiniteStageConjugacy line 76
  6. lemma OAI.SequentialCStar.System.conjugacy_difference_bound line 80
  7. theorem OAI.SequentialCStar.System.approximateConjugacy_iff_finiteStages line 87