OAI/RepresentationTheory/UniversalSquare/Capacity/RefinedCapacity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Refined Capacity.

  1. lemma OAI.UniversalTensorSquare.prefix_last_after_first line 15
  2. def OAI.UniversalTensorSquare.endpointBound line 27
  3. lemma OAI.UniversalTensorSquare.endpointBound_sound line 30
  4. lemma OAI.UniversalTensorSquare.prefix_intersection_hook line 45
  5. def OAI.UniversalTensorSquare.refinedArea line 80
  6. lemma OAI.UniversalTensorSquare.area_le_refined line 85