tendsto_smul_atImInfty — Mathlib

English

If g ∈ GL(2, ℝ) with g_{1,0} = 0, then the linear action τ ↦ g • τ sends atImInfty to atImInfty.

Русский

Если матрица g ∈ GL(2, ℝ) имеет нулевой элемент в позиции (1,0), то действие τ ↦ g • τ отправляет atImInfty в сам atImInfty.

LaTeX

$$$g \in GL(2, \mathbb{R}), \ g_{1 0} = 0 \implies \text{Tendsto}(\lambda \tau, g \cdot \tau) \text{ atImInfty }\text{ to } \text{atImInfty}$$$

Lean4

theorem tendsto_smul_atImInfty {g : GL (Fin 2) ℝ} (hg : g 1 0 = 0) : Tendsto (fun τ ↦ g • τ) atImInfty atImInfty :=
  by
  suffices Tendsto (fun τ ↦ |g 0 0 / g 1 1| * τ.im) atImInfty atTop by
    simpa [atImInfty, Function.comp_def, im_smul, num, denom, hg, abs_div, abs_mul,
      abs_of_pos (UpperHalfPlane.im_pos _), mul_div_right_comm]
  apply tendsto_comap.const_mul_atTop
  simpa [Matrix.det_fin_two, hg] using g.det_ne_zero

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