Specification.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Hyperinvariant.commutant line 14
Source documentation
The ordinary commutant in all bounded operators, not only in a chosen factor.
Also declared: ComparatorChallenges/HyperinvariantSubspaces.lean:16 (same declaration text).
```
def commutant (T : H →L[ℂ] H) : Subalgebra ℂ (H →L[ℂ] H) :=
…
```
def OAI.Hyperinvariant.TransitiveCommutant line 18
Source documentation
Closed common invariant subspaces, including all closed complex subspaces.
Also declared: ComparatorChallenges/HyperinvariantSubspaces.lean:19 (same declaration text).
```
def TransitiveCommutant (T : H →L[ℂ] H) : Prop :=
…
```
def OAI.Hyperinvariant.strongOperatorTopology line 24
Source documentation
Pointwise norm convergence restricted to bounded linear operators.
Also declared: ComparatorChallenges/HyperinvariantSubspaces.lean:24 (same declaration text).
```
@[instance_reducible] def strongOperatorTopology : TopologicalSpace (H →L[ℂ] H) :=
…
```
def OAI.Hyperinvariant.MainClaim line 28
Source documentation
Nonzero, norm-quasinilpotent, and with no nontrivial closed hyperinvariant subspace.
```
def MainClaim : Prop :=
…
```
def OAI.Hyperinvariant.FullClaim line 34
Source documentation
The same witness has a proper strongly closed unital complex commutant.
Also declared: ComparatorChallenges/HyperinvariantSubspaces.lean:27 (same declaration text).
```
def FullClaim : Prop :=
…
```