NormalStatePartitions.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Central partitions into pieces with normal states faithful on their centers.

theorem OAI.BoundedHochschild.KadisonRingrose.exists_central_normal_state_partition line 22
Source documentation
Every von Neumann algebra has a central partition into pieces detected faithfully on their centers by normal states. No traciality is asserted.
```
theorem exists_central_normal_state_partition (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M) :
    ∃ D : MaximalCentralPartition M (HasCentralFaithfulNormalState e),
      D.complement = 0 := by
…
```
Mentions: OAI.BoundedHochschild.KadisonRingrose.MaximalCentralPartition, OAI.BoundedHochschild.KadisonRingrose.HasCentralFaithfulNormalState