OAI/Topology/CoarseAssembly/ConcretePersistence.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Persistence with the geometric boundary input discharged

The actual six-side boundary walks are now substituted into the graph-family detector. Only the stated published circle pairing and countable-additivity inputs remain in the nonvanishing conclusions.

  1. def OAI.CoarseAssembly.concreteFiberClass line 22
  2. theorem OAI.CoarseAssembly.concreteFiberClass_infinite_order line 27
  3. theorem OAI.CoarseAssembly.concreteFiberClass_rational_ne_zero line 34