OAI/Computability/VertexCover/Reduction/IntegralCoe.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VertexCover.Restriction.plug line 43
  2. theorem OAI.VertexCover.Restriction.plug_empty line 46
  3. theorem OAI.VertexCover.Restriction.plug_univ line 49
  4. theorem OAI.VertexCover.Restriction.plug_insert_update line 52
  5. theorem OAI.VertexCover.Restriction.continuous_plug_right line 61
  6. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.product_average_apply line 75
  7. def OAI.VertexCover.Restriction.EnergyForm.Projection.averageSet line 92
  8. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.averageSet_apply line 96
  9. theorem OAI.VertexCover.Restriction.EnergyForm.Projection.averageSet_univ line 101
  10. theorem OAI.VertexCover.Restriction.restrict_preserving line 108
  11. theorem OAI.VertexCover.Restriction.integral_restrict line 122
  12. def OAI.VertexCover.Restriction.splice line 131
  13. theorem OAI.VertexCover.Restriction.continuous_splice_right line 134
  14. theorem OAI.VertexCover.Restriction.plug_erase_eq_splice_update line 142
  15. theorem OAI.VertexCover.Restriction.integral_plug_erase line 154
  16. abbrev OAI.VertexCover.Restriction.CompactCube.Interval line 167
  17. def OAI.VertexCover.Restriction.CompactCube.intervalLaw line 169
  18. theorem OAI.VertexCover.Restriction.CompactCube.ae_interval_mem line 172
  19. instance OAI.VertexCover.Restriction.CompactCube.(instance at line 176) line 176
  20. theorem OAI.VertexCover.Restriction.CompactCube.interval_preserving line 180
  21. def OAI.VertexCover.Restriction.CompactCube.law line 187
  22. instance OAI.VertexCover.Restriction.CompactCube.(instance at line 190) line 190
  23. def OAI.VertexCover.Restriction.CompactCube.realWeights line 194
  24. theorem OAI.VertexCover.Restriction.CompactCube.continuous_realWeights line 197
  25. theorem OAI.VertexCover.Restriction.CompactCube.law_preserving line 202
  26. def OAI.VertexCover.Restriction.CompactCube.blockLaw line 207
  27. instance OAI.VertexCover.Restriction.CompactCube.(instance at line 210) line 210
  28. theorem OAI.VertexCover.Restriction.CompactCube.blockLaw_preserving line 214
  29. theorem OAI.VertexCover.Restriction.CompactCube.integral_realWeights line 219
  30. theorem OAI.VertexCover.Restriction.CompactCube.integral_coe line 227