OAI/Analysis/StrictMeans/LatticeEuler.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StrictInverseFirstPower.Grid.natEmbed line 11
  2. lemma OAI.StrictInverseFirstPower.Grid.natEmbed_injective line 13
  3. lemma OAI.StrictInverseFirstPower.Grid.natEmbed_x line 19
  4. lemma OAI.StrictInverseFirstPower.Grid.natEmbed_y line 22
  5. lemma OAI.StrictInverseFirstPower.Grid.natEmbed_xy line 25
  6. lemma OAI.StrictInverseFirstPower.Grid.natEmbed_mx line 28
  7. lemma OAI.StrictInverseFirstPower.Grid.natEmbed_my line 31
  8. lemma OAI.StrictInverseFirstPower.Grid.natEmbed_coverage line 35
  9. lemma OAI.StrictInverseFirstPower.Grid.finite_natEmbed_coverage line 42
  10. lemma OAI.StrictInverseFirstPower.Grid.ncard_natEmbed_preimage line 51
  11. lemma OAI.StrictInverseFirstPower.Grid.lattice_sublevel_euler line 55
  12. lemma OAI.StrictInverseFirstPower.Grid.lattice_sublevel_index line 125