OAI/Combinatorics/EditDistance/CutRealization.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Realization of all finite-cut distances by one summable vector map

  1. def OAI.EditCutModel.Model.vector line 15
  2. lemma OAI.EditCutModel.singleton_sub_norm line 20
  3. lemma OAI.EditCutModel.Model.vector_distance line 35