English
Area form is compatible with maps between two-dim real inner product spaces, i.e., it commutes with pullbacks along linear isometries.
Русский
AreaForm совместима с отображениями между двумерными вещественными скалярно-произвольными пространствами, т.е. сохраняется при вытягивании по линейным изометриям.
LaTeX
$$AreaForm map commutes with pullback by isometry φ$$
Lean4
theorem areaForm_map {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [hF : Fact (finrank ℝ F = 2)]
(φ : E ≃ₗᵢ[ℝ] F) (x y : F) :
(Orientation.map (Fin 2) φ.toLinearEquiv o).areaForm x y = o.areaForm (φ.symm x) (φ.symm y) :=
by
have : φ.symm ∘ ![x, y] = ![φ.symm x, φ.symm y] := by
ext i
fin_cases i <;> rfl
simp [areaForm_to_volumeForm, volumeForm_map, this]
