OAI/Analysis/StrictMeans/IndexLocality.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StrictInverseFirstPower.Grid.meshStar line 11
  2. lemma OAI.StrictInverseFirstPower.Grid.mem_meshStar_self line 13
  3. lemma OAI.StrictInverseFirstPower.Grid.meshStar_symm line 15
  4. lemma OAI.StrictInverseFirstPower.Grid.heightIndex_congr_star line 25
  5. def OAI.StrictInverseFirstPower.Grid.meshBoundary line 37
  6. lemma OAI.StrictInverseFirstPower.Grid.mem_meshBoundary line 40
  7. lemma OAI.StrictInverseFirstPower.Grid.meshStar_subset_of_mem_not_boundary line 45
  8. lemma OAI.StrictInverseFirstPower.Grid.meshStar_disjoint_of_not_mem_not_boundary line 50
  9. lemma OAI.StrictInverseFirstPower.Grid.heightIndex_local_change line 57