qRight — Mathlib

English

Let p = (t, u) with t, u in the unit interval I. Then qRight(p) is obtained by applying the real projection of the affine expression 2t/(1+u) onto the closed interval [0,1].

Русский

Пусть p = (t, u) ∈ I × I. Тогда qRight(p) получается как проекция числа 2t/(1+u) на замкнутый интервал [0,1].

LaTeX

$$$qRight: I\times I \to I\quad\text{defined by}\quad qRight(p)=\mathrm{proj}_{[0,1]}\left(\dfrac{2 p_1}{1+p_2}\right).$$$

Lean4

/-- `qRight` is analogous to the function `Q` defined on p. 475 of [serre1951] that helps proving
continuity of `delayReflRight`. -/
def qRight (p : I × I) : I :=
  Set.projIcc 0 1 zero_le_one (2 * p.1 / (1 + p.2))

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