term↑ₕ_ — Mathlib

English

The upper-half-plane ℍ is locally compact.

Русский

Верхняя полуплоскость ℍ локально компактна.

LaTeX

$$$\\\\mathbb{H}$ is locally compact.$$

Lean4

/-- Extend a function on `ℍ` arbitrarily to a function on all of `ℂ`. -/
@[scoped term_parser 1000]
public meta def «term↑ₕ_» : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `UpperHalfPlane.«term↑ₕ_» 1022
    (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "↑ₕ") (ParserDescr.cat✝ `term 0))

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