exists_one_half_le_im_smul — Mathlib

English

Let τ ∈ ℍ. There exists γ ∈ SL(2,ℤ) with 1/2 ≤ im(γ•τ).

Русский

Пусть τ ∈ ℍ. Существует γ ∈ SL(2,ℤ) такое, что 1/2 ≤ im(γ•τ).

LaTeX

$$$\forall \tau \in \mathbb{H}, \exists \gamma\in SL(2,\mathbb{Z}), \tfrac{1}{2} \le \operatorname{im}(\gamma\cdot \tau)$$$

Lean4

theorem exists_one_half_le_im_smul (τ : ℍ) : ∃ γ : SL(2, ℤ), 1 / 2 ≤ im (γ • τ) :=
  by
  obtain ⟨γ, hγ⟩ := exists_smul_mem_fd τ
  use γ
  nlinarith [three_le_four_mul_im_sq_of_mem_fd hγ, im_pos (γ • τ)]

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