re_monotone

Mathlib.Analysis.RCLike.Basic

URI: https://scilib.ai/kg/mathlib#RCLike.re_monotone

English

Real part is a monotone map on K with respect to the order.

Русский

Действительная часть является монотонной по отношению к порядку на K.

LaTeX

$$$ \operatorname{re} \text{ is monotone on } K $$$

Lean4

theorem re_monotone : Monotone (re : K → ℝ) := fun _ _ => re_le_re

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

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

Разделы

Аффилиация

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