OAI/Analysis/IrrationalRotation/Operators/HyperfiniteCriterion.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Invariant233.HyperfiniteCriterion.asStrong line 16
2. theorem OAI.Invariant233.HyperfiniteCriterion.underlying_asStrong line 20
3. theorem OAI.Invariant233.HyperfiniteCriterion.asStrong_apply line 24
4. theorem OAI.Invariant233.HyperfiniteCriterion.mem_iSup_iff line 27
5. theorem OAI.Invariant233.HyperfiniteCriterion.strong_union_eq line 34
6. theorem OAI.Invariant233.HyperfiniteCriterion.mem_strong_union_closure_of_tendsto line 41
7. theorem OAI.Invariant233.HyperfiniteCriterion.strong_union_closure_subset line 52
8. theorem OAI.Invariant233.HyperfiniteCriterion.generated_iSup_eq_of_generator_approximation line 62