instContinuousGLSMul — Mathlib

English

Each element g ∈ GL(2,ℝ) defines a continuous map z ↦ g ⋅ z from ℍ to ℍ.

Русский

Каждый элемент g ∈ GL(2,ℝ) определяет непрерывное отображение z ↦ g · z: ℍ → ℍ.

LaTeX

$$$\\forall g \\in GL_2(\\\\mathbb{R}), \\\\ z \\\\mapsto g \\\\cdot z \\\\text{ is continuous on } \\\\mathbb{H}$.$$

Lean4

/-- Each element of `GL(2, ℝ)` defines a continuous map `ℍ → ℍ`. -/
instance instContinuousGLSMul : ContinuousConstSMul (GL (Fin 2) ℝ) ℍ where
  continuous_const_smul
    g :=
    by
    simp_rw [continuous_induced_rng (f := UpperHalfPlane.coe), Function.comp_def, UpperHalfPlane.coe_smul,
      UpperHalfPlane.σ]
    refine .comp ?_ ?_
    · split_ifs
      exacts [continuous_id, continuous_conj]
    · refine .div ?_ ?_ (fun x ↦ denom_ne_zero g x) <;> exact (continuous_const.mul continuous_coe).add continuous_const

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