OAI/NumberTheory/PiExponent/Approximation/SectionOpens.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PiExponentSeshadri.SectionOpens.isIso_of_stalks line 18
  2. lemma OAI.PiExponentSeshadri.SectionOpens.stalk_isIso_of_restrict line 29
  3. lemma OAI.PiExponentSeshadri.SectionOpens.restrict_isIso_of_stalks line 37
  4. lemma OAI.PiExponentSeshadri.SectionOpens.isIso_of_locally_isIso line 44
  5. def OAI.PiExponentSeshadri.SectionOpens.isoOpen line 53
  6. lemma OAI.PiExponentSeshadri.SectionOpens.mem_isoOpen_iff line 56
  7. theorem OAI.PiExponentSeshadri.SectionOpens.isIso_restrict_isoOpen line 62
  8. lemma OAI.PiExponentSeshadri.SectionOpens.isoOpen_postcomp line 76
  9. lemma OAI.PiExponentSeshadri.SectionOpens.isoOpen_precomp line 93
  10. lemma OAI.PiExponentSeshadri.SectionOpens.isoOpen_restrict line 110
  11. lemma OAI.PiExponentSeshadri.Frames.isUnit_iff_basicOpen_top line 144
  12. lemma OAI.PiExponentSeshadri.Frames.coefficient_restrict_isUnit line 153
  13. theorem OAI.PiExponentSeshadri.Frames.isoOpen_eq_basicOpen line 162
  14. lemma OAI.PiExponentSeshadri.Frames.isoOpen_restrictSection line 184
  15. theorem OAI.PiExponentSeshadri.Frames.preimage_isoOpen line 190