OAI/Analysis/KadisonKastler/FiniteType.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Discharging preservation of the finite diffuse type

A finite type I factor is finite dimensional. A nearby II₁ factor would then be finite dimensional as well, contradicting its projection splitting. Thus its finite neighboring factor is diffuse.

  1. theorem OAI.KadisonKastler.IsTypeIFactor.finiteDimensional line 23
  2. theorem OAI.KadisonKastler.publishedFiniteType line 46

    Source documentation

    The finite-neighbor type input follows from the constructed type I representation and the elementary finite-dimensional gap argument.

    theorem publishedFiniteType : PublishedFiniteType (H := H) := by
…

    Mentions: OAI.KadisonKastler.PublishedFiniteType