OAI/Geometry/Anticanonical/Liouville.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Constancy of equivariant analytic families from compact factors and lattice bounds.

  1. theorem OAI.DeckLiouville.exists_finite_injective_evaluations line 17
  2. theorem OAI.DeckLiouville.differentiable_of_evaluations line 47
  3. theorem OAI.DeckLiouville.equivariant_analytic_family_constant line 63
  4. theorem OAI.DeckLiouville.compact_factor_equivariant_family_constant line 102