OAI/Analysis/IrrationalRotation/Operators/NormalTraceDomainDensity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.NormalTraceDomainDensity.eq_of_le_of_trace_eq line 15
2. theorem OAI.Invariant233.NormalTraceDomainDensity.closure_inf_eq_of_normalizer line 36
3. theorem OAI.Invariant233.NormalTraceDomainDensity.closure_inf_domain_eq_of_normalizer line 72
4. theorem OAI.Invariant233.NormalTraceDomainDensity.closure_inf_domain_eq_of_affiliated line 84