OAI/Geometry/WeakMTW/Support/ActiveRepresentation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.WeakMTWGlobalSupport.WeakMTW.ActiveIndex line 24
2. structure OAI.WeakMTWGlobalSupport.WeakMTW.ActiveRepresentation line 26
3. theorem OAI.WeakMTWGlobalSupport.WeakMTW.activeRepresentation_exists line 37
4. theorem OAI.WeakMTWGlobalSupport.WeakMTW.activeRepresentation_subseq line 47