OAI/RepresentationTheory/VertexAlgebra/BicommutantOrbit.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.StronglyRationalVOA.BicommutantDensity.orbitMap line 11
2. def OAI.StronglyRationalVOA.BicommutantDensity.orbit line 16
3. instance OAI.StronglyRationalVOA.BicommutantDensity.orbit_isClosed line 19
4. theorem OAI.StronglyRationalVOA.BicommutantDensity.self_mem_orbit line 22
5. theorem OAI.StronglyRationalVOA.BicommutantDensity.orbit_invariant line 26
6. theorem OAI.StronglyRationalVOA.BicommutantDensity.projection_commutes_of_invariant line 36
7. theorem OAI.StronglyRationalVOA.BicommutantDensity.orbit_projection_mem_commutant line 48
8. theorem OAI.StronglyRationalVOA.BicommutantDensity.bicommutant_mem_orbit line 58
9. theorem OAI.StronglyRationalVOA.BicommutantDensity.exists_approx_one line 73