module module

`IndisputableMonolith.Cosmology.RegularNeighborhoodBoundary`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

declarations in this module (176)

structure BettiTriple L91
def regionEuler L98
def regularBoundaryComponents L102
def regularBoundaryEuler L106
def regularBoundaryGenus L110
def regularBoundaryCWVertices L117
def regularBoundaryCWEdges L121
def regularBoundaryCWFaces L125
def regularBoundaryCWEuler L129
theorem regularBoundaryGenus_eq_b1 L135
theorem regularBoundaryEuler_eq_two_regionEuler L141
theorem regularBoundaryCWEuler_eq_regularBoundaryEuler L147
theorem regularBoundaryCWEuler_eq_two_regionEuler L154
theorem components_minus_regionEuler_eq_b1 L160
structure IsRegularBoundaryOf L166
theorem genus_eq_b1_of_isRegularBoundaryOf L175
structure SingularGraphComponent L184
def halfVertexComponentDelta L191
def singularGraphHalfVertexDelta L195
def halfVertexCorrectedEuler L199
def HalfVertexQuotientCloses L204
theorem halfVertexCorrectedEuler_eq_cw_of_delta_eq_required L210
def singularV2E1 L221
def singularV4E3 L225
structure CorrectedBoundaryComponent L232
def correctedComponentCount L237
def correctedComponentEuler L241
def correctedComponentGenusFromHalfEuler L246
def ComponentAssemblyCloses L250
theorem correctedComponentGenus_eq_b1_of_componentAssemblyCloses L258
def sphereComponent L268
def torusComponent L272
def genus125Component L277
def horizonAnnulusHandleCorrectedComponents L281
def dyadicSpongeR20CorrectedComponents L285
structure PolygonGluingComponent L292
def PolygonComponentEulerOk L302
def PolygonComponentLinksCyclic L306
def polygonComponentToCorrected L310
def polygonComponentsToCorrected L314
def PolygonGluingCloses L319
theorem polygonGluedGenus_eq_b1_of_polygonGluingCloses L327
def horizonPolygonTorusComponent L336
def horizonPolygonSphereComponent L341
def horizonAnnulusHandlePolygonComponents L346
def dyadicPolygonGenus125Component L350
def dyadicPolygonSmallSphereComponent L355
def dyadicPolygonMediumSphereComponent L360
def dyadicPolygonLargeSphereComponent L365
def dyadicSpongeR20PolygonComponents L371
structure OrientedPolygonGluingComponent L382
def OrientedPolygonComponentOk L390
def orientedPolygonToPolygon L394
def orientedPolygonsToPolygons L398
def OrientedPolygonGluingCloses L404
theorem orientedPolygonGluedGenus_eq_b1_of_orientedPolygonGluingCloses L411
def horizonOrientedTorusComponent L421
def horizonOrientedSphereComponent L426
def horizonAnnulusHandleOrientedPolygonComponents L431
def dyadicOrientedGenus125Component L435
def dyadicOrientedSmallSphereComponent L440
def dyadicOrientedMediumSphereComponent L445
def dyadicOrientedLargeSphereComponent L450
def dyadicSpongeR20OrientedPolygonComponents L455
structure StandardSurfaceType L464
def standardSurfaceEuler L469
def PolygonComponentHasSurfaceType L474
def surfaceTypeGenusTotal L479
def surfaceTypeCount L483
def surfaceTypeEulerTotal L487
def orientedPolygonEulerList L491
def surfaceTypeEulerList L495
def orientedPolygonEulerTotal L499
theorem surfaceTypeEulerTotal_eq_count_genus L504
theorem correctedComponentCount_orientedPolygons L517
def SurfaceTypeClassificationCloses L527
theorem surfaceTypeGenusTotal_eq_b1_of_surfaceTypeClassificationCloses L537
theorem surfaceType_length_eq_orientedPolygon_length_of_surfaceTypeClassificationCloses L546
theorem orientedPolygonEulerList_eq_surfaceTypeEulerList_of_zip L560
theorem orientedPolygonEulerList_eq_surfaceTypeEulerList_of_surfaceTypeClassificationCloses L587

… and 96 more