OAI/Geometry/CylinderCovering/Barycentric/SectorNeighborhood.lean
11 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.RadialCoordinates.BarycentricSector.nearby_sector_point_in_triangleline 13 - theorem
OAI.RadialCoordinates.BarycentricSector.neighborhood_subset_triangleline 98 - def
OAI.RadialCoordinates.BarycentricSector.triangleCoordinateMapline 108 - theorem
OAI.RadialCoordinates.BarycentricSector.triangleCoordinateMap_detline 112 - theorem
OAI.RadialCoordinates.BarycentricSector.triangleChart_volumeline 116 - theorem
OAI.RadialCoordinates.BarycentricSector.neighborhoodTriangle_volumeline 132 - theorem
OAI.RadialCoordinates.BarycentricSector.neighborhoodTriangle_arealine 142 - theorem
OAI.RadialCoordinates.BarycentricSector.neighborhood_isCompactline 148 - theorem
OAI.RadialCoordinates.BarycentricSector.neighborhood_area_leline 153 - theorem
OAI.RadialCoordinates.BarycentricSector.neighborhood_area_errorline 161 - theorem
OAI.RadialCoordinates.BarycentricSector.intercepted_area_boundline 185