areaForm_neg_orientation

Mathlib.Analysis.InnerProductSpace.TwoDim

URI: https://scilib.ai/kg/mathlib#Orientation.areaForm_neg_orientation

English

Negating the orientation negates the area form: areaForm(-o) = - areaForm(o).

Русский

Смена ориентации на противоположную даёт противоположную площадной форме: areaForm(-o) = -areaForm(o).

LaTeX

$$areaForm_neg_orientation = areaForm(-o) = -areaForm(o)$$

Lean4

@[simp]
theorem areaForm_neg_orientation : (-o).areaForm = -o.areaForm :=
  by
  ext x y
  simp [areaForm_to_volumeForm]

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru