continuous — Mathlib

English

Any holomorphic modular form is continuous on the upper half-plane.

Русский

Любая голоморфная модулярная форма непрерывна на верхней полуплоскости.

LaTeX

$$$\forall f:\mathrm{ModularForm}(\Gamma,k),\; \mathrm{Continuous}(f)$$$

Lean4

@[fun_prop]
theorem continuous {k : ℤ} {Γ : Subgroup SL(2, ℤ)} {F : Type*} [FunLike F ℍ ℂ] [ModularFormClass F Γ k] (f : F) :
    Continuous f :=
  (ModularFormClass.holo f).continuous

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