uniformlyContinuous_im

Mathlib.Analysis.Complex.Basic

URI: https://scilib.ai/kg/mathlib#Complex.uniformlyContinuous_im

English

The imaginary part map is uniformly continuous; in particular, |Im z - Im w| ≤ |z - w|.

Русский

Мнимая часть отображения равномерно непрерывна; в частности, |Im z - Im w| ≤ |z - w|.

LaTeX

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

Lean4

theorem uniformlyContinuous_im : UniformContinuous im :=
  imCLM.uniformContinuous

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru