reflTransSymmAux — Mathlib

English

Auxiliary real-valued function used to reparametrize the path from trans to refl.

Русский

Вспомогательная функция на вещественных, используемая для перенормировки параметра траектории.

LaTeX

$$$ transReflReparamAux: I \to \mathbb{R} $$$

Lean4

/-- Auxiliary function for `reflTransSymm`. -/
def reflTransSymmAux (x : I × I) : ℝ :=
  if (x.2 : ℝ) ≤ 1 / 2 then x.1 * 2 * x.2 else x.1 * (2 - 2 * x.2)

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