OAI/Analysis/BackwardIntertwiners/ModelProperties.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.BackwardIntertwiners.OrdinaryStructuralProperties line 23
2. structure OAI.BackwardIntertwiners.PolarFamilyProperties line 40
3. def OAI.BackwardIntertwiners.PolarStructuralProperties line 64
4. lemma OAI.BackwardIntertwiners.coordinateTail_eq_closedSpan line 69
5. lemma OAI.BackwardIntertwiners.explicitDirectModel_ordinary line 93
6. lemma OAI.BackwardIntertwiners.explicitDirectModel_polarFamily line 103
7. theorem OAI.BackwardIntertwiners.direct_model_complete line 124