OAI/Analysis/KadisonKastler/FiniteInnerComposition.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Composition and scalar invariance of finite inner averages

  1. def OAI.KadisonKastler.FiniteInnerAverage.comp line 19

    Source documentation

    Applying one finite average after another is again a finite average.

    def comp (B A : FiniteInnerAverage M) : FiniteInnerAverage M where
…

    Mentions: OAI.KadisonKastler.FiniteInnerAverage

  2. theorem OAI.KadisonKastler.FiniteInnerAverage.comp_apply line 25
  3. theorem OAI.KadisonKastler.FiniteInnerAverage.apply_scalar line 53
  4. theorem OAI.KadisonKastler.FiniteInnerAverage.algebraApply_selfAdjoint line 64