OAI/Combinatorics/SparsestCut/FiniteNets.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.UniformSparsestCut.FiniteNets.euclidean_norm_le_sum_abs line 14
2. lemma OAI.UniformSparsestCut.FiniteNets.floor_coordinate_bound line 25
3. lemma OAI.UniformSparsestCut.FiniteNets.same_floor_distance line 40
4. theorem OAI.UniformSparsestCut.FiniteNets.exists_coordinate_net line 62
5. lemma OAI.UniformSparsestCut.FiniteNets.sphere_net_norm_bound line 94