OAI/Analysis/StrictMeans/GridSupport.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StrictInverseFirstPower.Grid.coeff line 10
  2. lemma OAI.StrictInverseFirstPower.Grid.coeff_sub line 12
  3. lemma OAI.StrictInverseFirstPower.Grid.coeff_x_zero line 15
  4. lemma OAI.StrictInverseFirstPower.Grid.coeff_x_succ line 17
  5. lemma OAI.StrictInverseFirstPower.Grid.coeff_y_zero line 19
  6. lemma OAI.StrictInverseFirstPower.Grid.coeff_y_succ line 21
  7. lemma OAI.StrictInverseFirstPower.Grid.finite_coeff_support line 24
  8. structure OAI.StrictInverseFirstPower.Grid.BoundarySupported line 33
  9. lemma OAI.StrictInverseFirstPower.Grid.BoundarySupported.anchor_eq line 38
  10. lemma OAI.StrictInverseFirstPower.Grid.BoundarySupported.anchor_zero_axis₁ line 43
  11. lemma OAI.StrictInverseFirstPower.Grid.BoundarySupported.anchor_zero_axis₂ line 49
  12. lemma OAI.StrictInverseFirstPower.Grid.BoundarySupported.anchor_eq_right line 54
  13. lemma OAI.StrictInverseFirstPower.Grid.BoundarySupported.anchor_eq_up line 60
  14. lemma OAI.StrictInverseFirstPower.Grid.BoundarySupported.anchor_eq_left line 66
  15. lemma OAI.StrictInverseFirstPower.Grid.BoundarySupported.anchor_eq_down line 72
  16. lemma OAI.StrictInverseFirstPower.Grid.BoundarySupported.anchor_zero_of_ascent line 78
  17. structure OAI.StrictInverseFirstPower.Grid.FaceSupported line 110
  18. lemma OAI.StrictInverseFirstPower.Grid.BoundarySupported.faceSupported line 114
  19. lemma OAI.StrictInverseFirstPower.Grid.cycle_fills_sublevel line 143