mk_neg — Mathlib

English

Negating z corresponds to negating the corresponding unit-disk element: mk(-z) equals - mk(z) with adjusted hz.

Русский

Отрицание z соответствует отрицанию элемента единичного диска: mk(-z) = - mk z с соответствующим hz.

LaTeX

$$$ \\forall z ∈ \\mathbb{C}, \\| -z \\| < 1 \\Rightarrow mk(-z) (\\| -z \\| < 1) = - mk(z) (\\| z \\| < 1). $$$$

Lean4

@[simp]
theorem mk_neg (z : ℂ) (hz : ‖-z‖ < 1) : mk (-z) hz = -mk z (norm_neg z ▸ hz) :=
  rfl

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