o — Mathlib · SciLib

English

A fixed positive orientation of the Euclidean plane R^2 is chosen and used to define oriented geometric notions.

Русский

Задаётся фиксированная положительная ориентация евклидового пространства \u211d^2, которая используется для определения ориентированных понятий геометрии.

LaTeX

$$$o = \\operatorname{positiveOrientation}$$$

Lean4

/-- A fixed choice of positive orientation of Euclidean space `ℝ²` -/
abbrev o :=
  @Module.Oriented.positiveOrientation

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