Plane linear area preserving bijective
ProvedBirkhoffGlobalSection.plane_linear_area_preserving_bijectivedifferential-geometryreal-analysis
A real-linear map of the coordinate plane preserving the signed area pairing is bijective.
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_linear_area_preserving_bijective :
∀ (A : Plane → Plane)
(hlin : ∀ (p r : Plane) (a b : ℝ), A (a • p + b • r) = a • A p + b • A r)
(harea : ∀ p r, A p 0 * A r 1 - A p 1 * A r 0 = p 0 * r 1 - p 1 * r 0),
Function.Bijective A := by sorrySource
Independent extraction of component 11 of the Proved theorem BirkhoffGlobalSection.variational_symplecticity_bundle. Original verified source: Solutions/Sol_BirkhoffGlobalSection_variational_symplecticity_bundle.lean. Exact original component retained.