OAI/Analysis/BackwardIntertwiners/HilbertClassification.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Hyperinvariant233.commutant line 12

   Also declared: ComparatorChallenges/BackwardIntertwiners.lean:11 (same declaration text).

2. def OAI.Hyperinvariant233.TransitiveCommutant line 16

   Also declared: ComparatorChallenges/BackwardIntertwiners.lean:14 (same declaration text).

3. def OAI.Hyperinvariant233.strongOperatorTopology line 23

   Also declared: ComparatorChallenges/BackwardIntertwiners.lean:20 (same declaration text).

4. def OAI.Hyperinvariant233.MainClaim line 27
5. def OAI.Hyperinvariant233.FullClaim line 33

   Also declared: ComparatorChallenges/BackwardIntertwiners.lean:23 (same declaration text).

6. theorem OAI.Hyperinvariant233.orthonormal_subtype_countable line 49
7. theorem OAI.Hyperinvariant233.exists_nat_hilbertBasis line 65
8. theorem OAI.Hyperinvariant233.nonempty_linearIsometryEquiv line 90