OAI/Analysis/ModularTheory/FiniteWeightDensity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Density of the concrete finite-weight GNS vectors.

  1. def OAI.WeakPureInfiniteness.modularFiniteWeightCut line 16
  2. lemma OAI.WeakPureInfiniteness.modularFiniteWeightMap_cut line 22
  3. lemma OAI.WeakPureInfiniteness.modularFiniteWeightMap_right_cut_tendsto line 33
  4. lemma OAI.WeakPureInfiniteness.modularFiniteWeightMap_dense line 41