normSq_S_smul_lt_one — Mathlib

English

If z ∈ ℍ and 1 < ∥z∥^2, then applying S to z yields ∥S•z∥^2 < 1.

Русский

Если z ∈ ℍ и 1 < ∥z∥^2, то S•z даёт ∥S•z∥^2 < 1.

LaTeX

$$$\\text{If } \\|z\\|^2 > 1,\\; \\|S\\cdot z\\|^2 < 1.$$$

Lean4

/-- If `1 < |z|`, then `|S • z| < 1`. -/
theorem normSq_S_smul_lt_one (h : 1 < normSq z) : normSq ↑(S • z) < 1 :=
  by
  rw [UpperHalfPlane.coe_specialLinearGroup_apply]
  simpa [coe_S, num, denom] using (inv_lt_inv₀ z.normSq_pos zero_lt_one).mpr h

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