OAI/Analysis/Commutator/MinimalOrbit.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.Kadison.CompactInvariant.invariant_closureline 20 - lemma
OAI.Kadison.CompactInvariant.invariant_orbitline 28 - lemma
OAI.Kadison.CompactInvariant.minimal_orbit_closureline 34 - lemma
OAI.Kadison.CompactInvariant.minimal_finite_open_coverline 47