OAI/Analysis/IrrationalRotation/Operators/BoundedRangeTrace.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Invariant233.BoundedRangeTrace.kernel_projection_mem line 10
2. theorem OAI.Invariant233.BoundedRangeTrace.kernel_trace_eq line 23
3. theorem OAI.Invariant233.BoundedRangeTrace.range_closure_eq line 52
4. theorem OAI.Invariant233.BoundedRangeTrace.range_trace_eq_of_injective line 56
5. theorem OAI.Invariant233.BoundedRangeTrace.preimage_trace_eq line 74
6. theorem OAI.Invariant233.BoundedRangeTrace.trace_le_transported_of_normalizer line 97
7. theorem OAI.Invariant233.BoundedRangeTrace.transported_trace_eq_of_normalizer line 128