OAI/Analysis/StrictMeans/GridLinear.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StrictInverseFirstPower.Grid.polyCoefficients line 10
  2. def OAI.StrictInverseFirstPower.Grid.coefficients line 13
  3. lemma OAI.StrictInverseFirstPower.Grid.coefficients_apply line 19
  4. def OAI.StrictInverseFirstPower.Grid.chainSpace line 21
  5. lemma OAI.StrictInverseFirstPower.Grid.mem_chainSpace line 24
  6. def OAI.StrictInverseFirstPower.Grid.chainSpaceEquiv line 36
  7. instance OAI.StrictInverseFirstPower.Grid.finite_chainSpace line 40
  8. lemma OAI.StrictInverseFirstPower.Grid.finrank_chainSpace line 43
  9. def OAI.StrictInverseFirstPower.Grid.horizontalSet line 49
  10. def OAI.StrictInverseFirstPower.Grid.verticalSet line 50
  11. def OAI.StrictInverseFirstPower.Grid.diagonalSet line 51
  12. def OAI.StrictInverseFirstPower.Grid.lowerSet line 52
  13. def OAI.StrictInverseFirstPower.Grid.upperSet line 53
  14. abbrev OAI.StrictInverseFirstPower.Grid.EdgeSpace line 55
  15. abbrev OAI.StrictInverseFirstPower.Grid.FaceSpace line 56
  16. def OAI.StrictInverseFirstPower.Grid.fullBoundary₁ line 58
  17. def OAI.StrictInverseFirstPower.Grid.fullBoundary₂ line 66