English
If f maps ball B(c,R) to itself and fixes c (f(c) = c), then dist(f(z), c) ≤ dist(z, c) for z in B(c,R).
Русский
Если f отображает шар в сам шар и фиксирует центр, то расстояние до центра не увеличивается: dist(f(z), c) ≤ dist(z, c).
LaTeX
$$$\mathrm{dist}(f(z), c) \le \mathrm{dist}(z, c)\quad (z \in \mathrm{ball}\ c\ R)$$$
Lean4
/-- The **Schwarz Lemma**: if `f : ℂ → ℂ` sends an open disk to itself and the center `c` of this
disk to itself, then for any point `z` of this disk we have `dist (f z) c ≤ dist z c`. -/
theorem dist_le_dist_of_mapsTo_ball_self (hd : DifferentiableOn ℂ f (ball c R))
(h_maps : MapsTo f (ball c R) (ball c R)) (hc : f c = c) (hz : z ∈ ball c R) : dist (f z) c ≤ dist z c :=
by
have := dist_le_div_mul_dist_of_mapsTo_ball hd (by rwa [hc]) hz
rwa [hc, div_self, one_mul] at this
exact (nonempty_ball.1 ⟨z, hz⟩).ne'
