OAI/Combinatorics/TreeEdit/DistortionTransfer.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TreeEdit.ratio_set_finite line 11
2. lemma OAI.TreeEdit.exists_realL1_injective line 17
3. lemma OAI.TreeEdit.c1_lower line 25
4. def OAI.TreeEdit.stretch line 33
5. def OAI.TreeEdit.contraction line 36
6. lemma OAI.TreeEdit.stretch_nonneg line 39
7. lemma OAI.TreeEdit.contraction_nonneg line 45
8. lemma OAI.TreeEdit.dist_le_stretch line 51
9. lemma OAI.TreeEdit.ed_le_contraction line 60
10. theorem OAI.TreeEdit.binary_transfer line 68