Obstruction.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.NuclearUltrapower.MainStatement line 15
Source documentation
Exact main obligation, using an existential representative of the universal C*-algebra. Proving this includes existence of C*(G), not just an implication from an assumed universal model, and includes its separability. The nonembedding assertion has no separability restriction on B.
```
def MainStatement : Prop :=
…
```
instance OAI.NuclearUltrapower.(instance at line 31) line 31
instance OAI.NuclearUltrapower.(instance at line 34) line 34
instance OAI.NuclearUltrapower.(instance at line 38) line 38
instance OAI.NuclearUltrapower.(instance at line 42) line 42
theorem OAI.NuclearUltrapower.main_statement line 49
Source documentation
The exact dyadic ambient group has a full group C*-algebra with the stated universal property, separability, and obstruction for every nuclear target.
```
theorem main_statement : MainStatement.{0} := by
…
```