OAI/Probability/LatticeSurface/Geometry/CapSmall.lean
11 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.ExtremalEdges.gradientBodyline 107 - lemma
OAI.ExtremalEdges.gradientBody_preimageline 111 - lemma
OAI.ExtremalEdges.compact_gradientBodyline 118 - lemma
OAI.ExtremalEdges.convex_gradientBodyline 125 - lemma
OAI.ExtremalEdges.neg_gradientBodyline 142 - lemma
OAI.ExtremalEdges.central_gradientBodyline 148 - def
OAI.ExtremalEdges.capsIntervalline 155 - lemma
OAI.ExtremalEdges.measurable_capsIntervalline 157 - lemma
OAI.ExtremalEdges.mem_capsIntervalline 160 - lemma
OAI.ExtremalEdges.volume_capsIntervalline 169 - theorem
OAI.ExtremalEdges.star_cap_volumeline 176