OAI/AlgebraicGeometry/NumericalDimension/KltMembers.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Klt Members.

  1. def OAI.NumericalDimensionOne.IsKltBoundary line 23
  2. lemma OAI.NumericalDimensionOne.IsCartierPullback.zsmul line 36
  3. lemma OAI.NumericalDimensionOne.IsCartierPullback.rational line 46
  4. lemma OAI.NumericalDimensionOne.IsQCartierPullback.smul line 53
  5. theorem OAI.NumericalDimensionOne.smooth_boundary_isKlt line 64
  6. lemma OAI.NumericalDimensionOne.constructible_constant_near_generic line 114
  7. theorem OAI.NumericalDimensionOne.finiteType_generic_smooth_open line 134
  8. theorem OAI.NumericalDimensionOne.exists_avoiding_countable_polynomials line 170
  9. lemma OAI.NumericalDimensionOne.exists_rational_tuple_in_countable_spec_opens line 225
  10. theorem OAI.NumericalDimensionOne.exists_rational_point_in_countable_affine_opens line 249
  11. theorem OAI.NumericalDimensionOne.exists_smooth_fiber_in_countable_opens line 291
  12. theorem OAI.NumericalDimensionOne.exists_linear_nonvanishing_parameter_open line 350
  13. lemma OAI.NumericalDimensionOne.linearMemberSection_evaluate line 389
  14. theorem OAI.NumericalDimensionOne.exists_parameter_open_avoiding_point line 421
  15. theorem OAI.NumericalDimensionOne.incidence_parameter_open_avoiding_point line 465
  16. theorem OAI.NumericalDimensionOne.incidence_smooth_baseChange line 507
  17. theorem OAI.NumericalDimensionOne.exists_very_general_incidence_member line 542
  18. lemma OAI.NumericalDimensionOne.parameter_member_comap line 591
  19. theorem OAI.NumericalDimensionOne.exists_very_general_incidence_member_on_open line 598
  20. theorem OAI.NumericalDimensionOne.closed_set_finite_generics line 637