OAI/Analysis/StrictMeans/TriangularIndex.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StrictInverseFirstPower.Grid.rankBit line 11
  2. lemma OAI.StrictInverseFirstPower.Grid.rankBit_complement line 13
  3. def OAI.StrictInverseFirstPower.Grid.topBit line 18
  4. lemma OAI.StrictInverseFirstPower.Grid.topBit_sum line 20
  5. lemma OAI.StrictInverseFirstPower.Grid.ne_self_add_of_ne_zero line 33
  6. def OAI.StrictInverseFirstPower.Grid.edgeFlag line 37
  7. def OAI.StrictInverseFirstPower.Grid.lowerTop₀ line 39
  8. def OAI.StrictInverseFirstPower.Grid.lowerTop₁ line 40
  9. def OAI.StrictInverseFirstPower.Grid.lowerTop₂ line 41
  10. def OAI.StrictInverseFirstPower.Grid.upperTop₀ line 42
  11. def OAI.StrictInverseFirstPower.Grid.upperTop₁ line 43
  12. def OAI.StrictInverseFirstPower.Grid.upperTop₂ line 44
  13. lemma OAI.StrictInverseFirstPower.Grid.lowerTop_sum line 46
  14. lemma OAI.StrictInverseFirstPower.Grid.upperTop_sum line 54
  15. def OAI.StrictInverseFirstPower.Grid.meshIndex line 62
  16. lemma OAI.StrictInverseFirstPower.Grid.meshIndex_eq_linkIndex line 69
  17. lemma OAI.StrictInverseFirstPower.Grid.meshIndex_eq_divergence line 81