mk — Mathlib · SciLib

English

There is a canonical way to form an element of 𝔻 from a complex z with ‖z‖ < 1.

Русский

Существует канонический способ получить элемент 𝔻 из z ∈ ℂ с ‖z‖ < 1.

LaTeX

$$$ 𝔻 \\cong \\{ z \\in \\mathbb{C} : |z| < 1 \\} $$$

Lean4

/-- A constructor that assumes `‖z‖ < 1` instead of `dist z 0 < 1` and returns an element
of `𝔻` instead of `↥Metric.ball (0 : ℂ) 1`. -/
def mk (z : ℂ) (hz : ‖z‖ < 1) : 𝔻 :=
  ⟨z, mem_ball_zero_iff.2 hz⟩

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