OAI/Analysis/KadisonKastler/BoundedFamilyCurry.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Bounded currying for two discrete group coordinates

  1. def OAI.KadisonKastler.boundedFamilyRow line 18
  2. theorem OAI.KadisonKastler.boundedFamilyRow_apply line 24
  3. theorem OAI.KadisonKastler.boundedFamilyRow_norm_le line 28
  4. def OAI.KadisonKastler.boundedFamilyCurry line 32
  5. theorem OAI.KadisonKastler.boundedFamilyCurry_apply line 38
  6. def OAI.KadisonKastler.boundedFamilyCurryL line 41
  7. theorem OAI.KadisonKastler.boundedFamilyCurryL_apply line 52