norm_le_norm_of_mapsTo_ball_self — Mathlib

English

If f maps the unit ball around 0 into itself and f(0) = 0, then ‖f(z)‖ ≤ ‖z‖ for z in the ball.

Русский

Если f отображает единичный шар вокруг нуля в сам шар и f(0) = 0, то ‖f(z)‖ ≤ ‖z‖.

LaTeX

$$$\|f(z)\| \le \|z\|$$$

Lean4

/-- The **Schwarz Lemma**: if `f : ℂ → ℂ` sends an open disk with center `0` to itself, then for any
point `z` of this disk we have `‖f z‖ ≤ ‖z‖`. -/
theorem norm_le_norm_of_mapsTo_ball_self (hd : DifferentiableOn ℂ f (ball 0 R))
    (h_maps : MapsTo f (ball 0 R) (ball 0 R)) (h₀ : f 0 = 0) (hz : ‖z‖ < R) : ‖f z‖ ≤ ‖z‖ :=
  by
  replace hz : z ∈ ball (0 : ℂ) R := mem_ball_zero_iff.2 hz
  simpa only [dist_zero_right] using dist_le_dist_of_mapsTo_ball_self hd h_maps h₀ hz

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