re_le_re

Mathlib.Analysis.Complex.Basic

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

English

For all x ∈ ℂ, the real-valued linear functional re equals the real component of x, i.e., reC x = x.re.

Русский

Для всех x ∈ ℂ действительная часть функции равна действительной части x: reC x = x.re.

LaTeX

$$$reC\,x = x.re$$$

Lean4

@[gcongr]
theorem re_le_re {x y : ℂ} (h : x ≤ y) : re x ≤ re y :=
  by
  rw [RCLike.le_iff_re_im] at h
  exact h.1

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

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

Разделы

Аффилиация

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