mk — Mathlib · SciLib

English

Constructor for UpperHalfPlane: given z ∈ ℂ and h with h > 0, produce an element of the upper half-plane.

Русский

Конструктор для UpperHalfPlane: задано z ∈ ℂ и h > 0, получить элемент верхней полуплоскости.

LaTeX

$$mk : (z : \mathbb{C}) → (h : 0 < z.im) → \mathbb{H}$$

Lean4

/-- Constructor for `UpperHalfPlane`. It is useful if `⟨z, h⟩` makes Lean use a wrong
typeclass instance. -/
def mk (z : ℂ) (h : 0 < z.im) : ℍ :=
  ⟨z, h⟩

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