OAI/NumberTheory/PiExponent/Ampleness/ExceptionalAffineChartRestriction.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PiExponent.ExceptionalAffineChart.schemeFreeOpen line 14

    Distinct definitions of this name: OAI/NumberTheory/PiExponent/Ampleness/ExceptionalRepresentedOpaque.lean:10 (same statement text; different proof or body). Qualify references as OAI.PiExponent.ExceptionalAffineChart.schemeFreeOpen@path.

  2. lemma OAI.PiExponent.ExceptionalAffineChart.opensRange_le line 24
  3. lemma OAI.PiExponent.ExceptionalAffineChart.chart_square line 30
  4. def OAI.PiExponent.ExceptionalAffineChart.functionsOnOpenEquiv line 36
  5. lemma OAI.PiExponent.ExceptionalAffineChart.chartFunctions_naturality line 39
  6. lemma OAI.PiExponent.ExceptionalAffineChart.topIso_restriction line 54
  7. lemma OAI.PiExponent.ExceptionalAffineChart.functionsOnOpenEquiv_naturality line 66
  8. theorem OAI.PiExponent.ExceptionalAffineChart.restrictedInclusion_value line 79
  9. def OAI.PiExponent.ExceptionalAffineChart.sectionsOnOpenEquiv line 97
  10. theorem OAI.PiExponent.ExceptionalAffineChart.sectionsOnOpenEquiv_apply line 102
  11. def OAI.PiExponent.ExceptionalAffineChart.representedSectionsEquiv line 112
  12. theorem OAI.PiExponent.ExceptionalAffineChart.sectionsOnOpenEquiv_restrict line 126
  13. theorem OAI.PiExponent.ExceptionalAffineChart.representedSectionsEquiv_restrict line 141