OAI/Analysis/StrictMeans/LatticeIndex.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.StrictInverseFirstPower.Grid.Lattice line 10
  2. def OAI.StrictInverseFirstPower.Grid.ex line 11
  3. def OAI.StrictInverseFirstPower.Grid.ey line 12
  4. def OAI.StrictInverseFirstPower.Grid.latticeHeight line 14
  5. lemma OAI.StrictInverseFirstPower.Grid.ex_ne_zero line 16
  6. lemma OAI.StrictInverseFirstPower.Grid.ey_ne_zero line 17
  7. lemma OAI.StrictInverseFirstPower.Grid.ex_add_ey_ne_zero line 18
  8. lemma OAI.StrictInverseFirstPower.Grid.bool_congr line 20
  9. lemma OAI.StrictInverseFirstPower.Grid.separable_strict_bits line 23
  10. lemma OAI.StrictInverseFirstPower.Grid.separable_weak_bits line 31
  11. lemma OAI.StrictInverseFirstPower.Grid.separable_linkIndex line 39
  12. lemma OAI.StrictInverseFirstPower.Grid.heightRank_pos_x line 49
  13. lemma OAI.StrictInverseFirstPower.Grid.heightRank_pos_y line 55
  14. lemma OAI.StrictInverseFirstPower.Grid.heightRank_pos_xy line 61
  15. lemma OAI.StrictInverseFirstPower.Grid.heightRank_neg_step line 69
  16. lemma OAI.StrictInverseFirstPower.Grid.latticeHeight_index line 76