circleEquivGen_apply — Mathlib

English

The apply form of circleEquivGen hk is (2x)/(1+x^2) for the first coordinate and (1−x^2)/(1+x^2) for the second.

Русский

Обозначение применения circleEquivGen hk для точки на окружности даёт координаты (2x)/(1+x^2) и (1−x^2)/(1+x^2).

LaTeX

$$$(circleEquivGen hk x) = \langle \tfrac{2x}{1+x^2}, \tfrac{1-x^2}{1+x^2} \rangle$$$

Lean4

@[simp]
theorem circleEquivGen_apply (hk : ∀ x : K, 1 + x ^ 2 ≠ 0) (x : K) :
    (circleEquivGen hk x : K × K) = ⟨2 * x / (1 + x ^ 2), (1 - x ^ 2) / (1 + x ^ 2)⟩ :=
  rfl

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