Plane area preserving injective
ProvedBirkhoffGlobalSection.plane_area_preserving_injectivedifferential-geometryreal-analysis
Any map of the real coordinate plane preserving the signed area pairing of every two input vectors is injective; linearity is not an assumption.
All displayed regularity, tangency, normalization and supplied-data hypotheses of the exact formal statement are retained.
Preamble
import Theorems.Thm_BirkhoffGlobalSection_variational_symplecticity_bundle open BirkhoffGlobalSection Set Filter Topology open scoped ContDiff Topology set_option linter.unusedVariables false set_option autoImplicit false set_option maxHeartbeats 800000
Formal statement
theorem BirkhoffGlobalSection.plane_area_preserving_injective :
∀ (A : Plane → Plane)
(hA : ∀ p r, A p 0 * A r 1 - A p 1 * A r 0 = p 0 * r 1 - p 1 * r 0),
Function.Injective A := by sorrySource
Independent extraction of component 10 of the Proved theorem BirkhoffGlobalSection.variational_symplecticity_bundle. Original verified source: Solutions/Sol_BirkhoffGlobalSection_variational_symplecticity_bundle.lean. Exact original component retained.