Theorems · Definition · geometry

Orientation.areaForm

{E : Type u_2} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : InnerProductSpace ℝ E] → [Fact (Module.finrank ℝ E = 2)] → Orientation ℝ E (Fin 2) → E →ₗ[ℝ] E →ₗ[ℝ] ℝ

An antisymmetric bilinear form on an oriented real inner product space of dimension 2 (usual notation ω). When evaluated on two vectors, it gives the oriented area of the parallelogram they span.

Defined in

Mathlib.Analysis.InnerProductSpace.TwoDim

Cited by

44 results in Mathlib

Foundations

Depth 249 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupInnerProductSpaceFact