OAI/AlgebraicGeometry/NumericalDimension/LocalKltMembers.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Local Klt Members.

  1. structure OAI.NumericalDimensionOne.DivisorOpenAtlas line 28
  2. def OAI.NumericalDimensionOne.DivisorOpenAtlas.cover line 38
  3. instance OAI.NumericalDimensionOne.DivisorOpenAtlas.(instance at line 47) line 47
  4. instance OAI.NumericalDimensionOne.DivisorOpenAtlas.(instance at line 48) line 48
  5. def OAI.NumericalDimensionOne.DivisorOpenAtlas.coordinate line 49
  6. lemma OAI.NumericalDimensionOne.DivisorOpenAtlas.cover_comp line 51
  7. theorem OAI.NumericalDimensionOne.exists_divisorOpenAtlas line 55
  8. theorem OAI.NumericalDimensionOne.DivisorOpenAtlas.exists_nonzero_smooth_member line 73
  9. theorem OAI.NumericalDimensionOne.exists_effective_member_smooth_on_open line 136
  10. theorem OAI.NumericalDimensionOne.order_smooth_hypersurface_le_jacobian line 210
  11. lemma OAI.NumericalDimensionOne.order_smooth_hypersurface_le_jacobian_chart line 248
  12. lemma OAI.NumericalDimensionOne.cartier_order_le_jacobian_of_chart line 276
  13. lemma OAI.NumericalDimensionOne.topDifferentialMap_scalar_chart line 320
  14. theorem OAI.NumericalDimensionOne.smooth_boundary_discrepancy_bound_at line 339
  15. theorem OAI.NumericalDimensionOne.exists_effective_locally_klt_member line 486