OAI/RepresentationTheory/VertexAlgebra/NormalUniqueness.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.StronglyRationalVOA.LocalOperatorAlgebra.vonNeumann_isClosed line 15
2. theorem OAI.StronglyRationalVOA.LocalOperatorAlgebra.IsNormal.tendsto_net line 20
3. theorem OAI.StronglyRationalVOA.LocalOperatorAlgebra.normal_eq_of_bounded_net line 33
4. theorem OAI.StronglyRationalVOA.BicommutantDensity.normal_eq_selfAdjoint line 56