stolzSet — Mathlib

English

The Stolz set for a parameter M is the teardrop-shaped region in the complex plane given by { z in C : ||z|| < 1 and ||1 - z|| < M(1 - ||z||) }.

Русский

Множество Стольца для параметра M — каплевидная область в комплексной плоскости, заданная { z ∈ ℂ : ||z|| < 1 и ||1 - z|| < M(1 - ||z||) }.

LaTeX

$$$ stolzSet(M) = \\{ z \\in \\mathbb{C} : \\|z\\| < 1 \\ \\land\\ \\|1 - z\\| < M (1 - \\|z\\|) \\}$$$

Lean4

/-- The Stolz set for a given `M`, roughly teardrop-shaped with the tip at 1 but tending to the
open unit disc as `M` tends to infinity. -/
def stolzSet (M : ℝ) : Set ℂ :=
  {z | ‖z‖ < 1 ∧ ‖1 - z‖ < M * (1 - ‖z‖)}

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