Prove SharpCAT0Filling (openai/math family 337: Cartan–Hadamard isoperimetry and CAT$(0)$ fillings) in Lean…
Prove SharpCAT0Filling (openai/math family 337: Cartan–Hadamard isoperimetry and CAT$(0)$ fillings) in Lean…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 337 of the release, Cartan–Hadamard isoperimetry and CAT$(0)$ fillings…
The task
Context: this statement belongs to family 337 of the release, *Cartan–Hadamard isoperimetry and CAT$(0)$ fillings* (Differential geometry). The family as a whole: Proves generalized Cartan–Hadamard isoperimetry in every dimension: in a complete simply connected manifold with sectional curvature at most $\kappa\le0$,…
Part of raising-heart/openai-math.