stolzCone — Mathlib

English

The Stolz cone is the left-sided cone defined by { z in C : |Im z| < s(1 - Re z) } for a given slope s.

Русский

Конус Стольца — левый конус, задаваемый { z ∈ ℂ : |Im z| < s(1 - Re z) } для данного угла наклона s.

LaTeX

$$$ stolzCone(s) = \\{ z \\in \\mathbb{C} : |\\operatorname{Im} z| < s\\,(1 - \\operatorname{Re} z) \\}$$$

Lean4

/-- The cone to the left of `1` with angle `2θ` such that `tan θ = s`. -/
def stolzCone (s : ℝ) : Set ℂ :=
  {z | |z.im| < s * (1 - z.re)}

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