OAI/Computability/VertexCover/Reduction/CoordinateProductInvariant.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.VertexCover.Restriction.EnergyForm.Projection.coordinateKey line 43
2. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.coordinateKey_update line 46
3. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.coordinateKey_eq_iff line 51
4. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.coordinateKey_fiber line 70
5. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.conditionMap_coordinate line 88
6. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.conditionMap_coordinate_commute line 108
7. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.invariant_of_coordinate_invariant line 126
8. def OAI.VertexCover.Restriction.EnergyForm.Projection.coordinateCondition line 148
9. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.coordinateCondition_commute line 151
10. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.coordinate_product_invariant line 159