uniformlyContinuous_re — Mathlib

English

The real part map is uniformly continuous; in particular, |Re z - Re w| ≤ |z - w| for all z,w.

Русский

Отображение вещественной части равномерно непрерывно; в частности, для всех z,w выполняется |Re z - Re w| ≤ |z - w|.

LaTeX

$$$$ |\\Re z - \\Re w| \\le |z - w| \\quad \\text{for all } z,w \\in \\mathbb{C}. $$$$

Lean4

theorem uniformlyContinuous_re : UniformContinuous re :=
  reCLM.uniformContinuous

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