CylinderWeights.lean`

GitHub source file

85 declarations, 0 contain sorry, 0 declared as axioms

Cylinder Weights.

lemma OAI.Thomason.GrayRecursive.IntervalHom.face_false line 16
lemma OAI.Thomason.GrayRecursive.IntervalHom.bounded_iff_fixed line 20
lemma OAI.Thomason.GrayRecursive.IntervalHom.restrictCylinder_post line 24
def OAI.Thomason.GrayRecursive.IntervalHom.mapCell line 29
lemma OAI.Thomason.GrayRecursive.IntervalHom.eval_mapCell line 35
lemma OAI.Thomason.GrayRecursive.IntervalHom.mapCell_ofMap line 38
lemma OAI.Thomason.GrayRecursive.IntervalHom.mapCell_face line 42
lemma OAI.Thomason.GrayRecursive.IntervalHom.mapCell_comp line 48
def OAI.Thomason.GrayRecursive.IntervalHom.mapFunctor line 62
def OAI.Thomason.GrayRecursive.IntervalHom.functor line 68
def OAI.Thomason.GrayRecursive.IntervalHom.cellsEquiv line 74
lemma OAI.Thomason.GrayRecursive.IntervalHom.presentation_separates line 91
def OAI.Thomason.GrayRecursive.IntervalHom.TensorGenerator line 103
def OAI.Thomason.GrayRecursive.IntervalHom.tensorPresentation line 105
lemma OAI.Thomason.GrayRecursive.IntervalHom.functor_cell_bounded line 113
def OAI.Thomason.GrayRecursive.IntervalHom.tensorInterpretation line 118
def OAI.Thomason.GrayRecursive.IntervalHom.generatorCylinder line 127
lemma OAI.Thomason.GrayRecursive.IntervalHom.generatorCylinder_interpretation line 154
lemma OAI.Thomason.GrayRecursive.IntervalHom.ofMap_generator_image line 161
def OAI.Thomason.GrayRecursive.IntervalHom.tensorUnitCell line 169
lemma OAI.Thomason.GrayRecursive.IntervalHom.tensorUnitCell_image line 172
lemma OAI.Thomason.GrayRecursive.IntervalHom.tensorUnitCell_of_bounded line 179
lemma OAI.Thomason.GrayRecursive.IntervalHom.tensorUnitCell_source line 186
lemma OAI.Thomason.GrayRecursive.IntervalHom.tensorUnitCell_target line 196
lemma OAI.Thomason.GrayRecursive.IntervalHom.tensorUnitCell_comp line 206
def OAI.Thomason.GrayRecursive.IntervalHom.tensorUnit line 226
def OAI.Thomason.GrayRecursive.IntervalHom.uncurry line 244
def OAI.Thomason.GrayRecursive.IntervalHom.curry line 248
lemma OAI.Thomason.GrayRecursive.IntervalHom.curry_uncurry line 252
lemma OAI.Thomason.GrayRecursive.IntervalHom.curry_eval line 257
lemma OAI.Thomason.GrayRecursive.IntervalHom.uncurry_curry line 264
def OAI.Thomason.GrayRecursive.IntervalHom.homEquiv line 269
lemma OAI.Thomason.GrayRecursive.IntervalHom.homEquiv_natural line 276
def OAI.Thomason.GrayRecursive.IntervalHom.tensorFunctor line 279
def OAI.Thomason.GrayRecursive.IntervalHom.tensorAdjunction line 282
instance OAI.Thomason.GrayRecursive.IntervalHom.tensorFunctor_isLeftAdjoint line 285
instance OAI.Thomason.GrayRecursive.IntervalHom.tensorFunctor_preservesColimits line 286
lemma OAI.Thomason.GrayRecursive.IntervalHom.tensorFunctor_obj line 289
lemma OAI.Thomason.GrayRecursive.IntervalHom.tensorFunctor_map_generator line 291
lemma OAI.Thomason.GrayRecursive.IntervalHom.endpointTop_bounded line 309
def OAI.Thomason.GrayRecursive.IntervalHom.endpointCell line 315
lemma OAI.Thomason.GrayRecursive.IntervalHom.endpointCell_of_bounded line 318
lemma OAI.Thomason.GrayRecursive.IntervalHom.endpointCell_ofMap line 327
lemma OAI.Thomason.GrayRecursive.IntervalHom.endpointCell_face line 331
lemma OAI.Thomason.GrayRecursive.IntervalHom.endpointCell_comp line 337
def OAI.Thomason.GrayRecursive.IntervalHom.endpointFunctor line 350
lemma OAI.Thomason.GrayRecursive.IntervalHom.endpointCell_map line 356
def OAI.Thomason.GrayRecursive.IntervalHom.endpointTransformation line 363
def OAI.Thomason.GrayRecursive.IntervalHom.tensorEndpoint line 367
lemma OAI.Thomason.GrayRecursive.IntervalHom.tensorEndpoint_bounded line 378
lemma OAI.Thomason.GrayRecursive.IntervalHom.constantInterval_restrict line 395
lemma OAI.Thomason.GrayRecursive.IntervalHom.lift_face line 402
lemma OAI.Thomason.GrayRecursive.IntervalHom.constant_bound_mono line 410
lemma OAI.Thomason.GrayRecursive.IntervalHom.constant_bound_independent line 420
def OAI.Thomason.GrayRecursive.IntervalHom.constantCell line 425
lemma OAI.Thomason.GrayRecursive.IntervalHom.constantCell_of_bounded line 428
lemma OAI.Thomason.GrayRecursive.IntervalHom.constantCell_face line 432
lemma OAI.Thomason.GrayRecursive.IntervalHom.constantCell_comp line 439
def OAI.Thomason.GrayRecursive.IntervalHom.constantFunctor line 460
lemma OAI.Thomason.GrayRecursive.IntervalHom.constantCell_map line 466
def OAI.Thomason.GrayRecursive.IntervalHom.constantTransformation line 479
lemma OAI.Thomason.GrayRecursive.IntervalHom.endpointCell_constant line 483
def OAI.Thomason.GrayRecursive.IntervalHom.tensorProjection line 487
lemma OAI.Thomason.GrayRecursive.IntervalHom.tensorProjection_generator line 500
lemma OAI.Thomason.GrayRecursive.IntervalHom.tensorEndpoint_projection line 507
def OAI.Thomason.GrayRecursive.IntervalHom.globeDiagram line 525
lemma OAI.Thomason.GrayRecursive.IntervalHom.globeDiagram_top line 529
lemma OAI.Thomason.GrayRecursive.IntervalHom.globeDiagram_face line 533
lemma OAI.Thomason.GrayRecursive.IntervalHom.globeDiagram_map line 538
def OAI.Thomason.GrayRecursive.IntervalHom.globeTensorHom line 560
def OAI.Thomason.GrayRecursive.IntervalHom.globeTensorInv line 563
lemma OAI.Thomason.GrayRecursive.IntervalHom.globeTensorHom_generator line 566
lemma OAI.Thomason.GrayRecursive.IntervalHom.globeTensorHom_inv line 570
lemma OAI.Thomason.GrayRecursive.IntervalHom.globeTensorInv_hom line 582
def OAI.Thomason.GrayRecursive.IntervalHom.globeTensorIso line 589
lemma OAI.Thomason.GrayRecursive.IntervalHom.globeTensorIso_natural line 595
lemma OAI.Thomason.GrayRecursive.IntervalHom.globeTensorIso_endpoint line 614
lemma OAI.Thomason.GrayRecursive.IntervalHom.globeTensorIso_projection line 623
structure OAI.Thomason.GrayRecursive.CellWeight line 651
instance OAI.Thomason.GrayRecursive.CellWeight.(instance at line 659) line 659
def OAI.Thomason.GrayRecursive.CellWeight.hom line 661
def OAI.Thomason.GrayRecursive.CellWeight.row line 669
lemma OAI.Thomason.GrayRecursive.concatInterval_weight line 679
lemma OAI.Thomason.GrayRecursive.horizontalCylinder_weight line 705
lemma OAI.Thomason.GrayRecursive.pasteCylinder_weight line 746