OAI/Combinatorics/ThinTrees/BagGeometry.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.StrongThinTree.Geometry.distance_balls_disjointline 18 - lemma
OAI.StrongThinTree.Geometry.l1_separated_netline 31 - lemma
OAI.StrongThinTree.Geometry.retain_fibersline 70 - lemma
OAI.StrongThinTree.Geometry.compact_from_netline 119 - lemma
OAI.StrongThinTree.Geometry.normalized_small_ballsline 221