OAI/Analysis/FreeWords/ProjectionStructure.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KKProjectionSupport.concrete_projection_coe line 19
2. theorem OAI.KKProjectionSupport.exists_maximal_concrete_partialIso line 23
3. theorem OAI.KKProjectionSupport.factor_partial_in_corner line 39
4. theorem OAI.KKProjectionSupport.projection_comparable_by_trace line 55
5. theorem OAI.KKProjectionSupport.projection_equivalent_of_trace line 96