OAI/Topology/ArtinGroups/Realizations/WeightHomeomorph.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HarmonicArtin.weightHomeomorph line 12
  2. lemma OAI.HarmonicArtin.weightMap_vertex line 26
  3. def OAI.HarmonicArtin.weightSubset line 30
  4. lemma OAI.HarmonicArtin.weightSubset_comp line 33
  5. lemma OAI.HarmonicArtin.weightSubset_incl line 35
  6. lemma OAI.HarmonicArtin.weightSubset_self line 38
  7. def OAI.HarmonicArtin.transportContraction line 40
  8. structure OAI.HarmonicArtin.WeightContractionPiece line 51
  9. def OAI.HarmonicArtin.WeightContractionPiece.inclusion line 60
  10. def OAI.HarmonicArtin.WeightContractionPiece.Extends line 62
  11. lemma OAI.HarmonicArtin.WeightContractionPiece.extends_refl line 67
  12. lemma OAI.HarmonicArtin.WeightContractionPiece.extends_trans line 72
  13. lemma OAI.HarmonicArtin.WeightContractionPiece.extends_compare line 80