re_le_re

Mathlib.Analysis.RCLike.Basic

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

English

If x ≤ y in K, then Re(x) ≤ Re(y).

Русский

Если x ≤ y в K, то Re(x) ≤ Re(y).

LaTeX

$$$ x \le y \Rightarrow \operatorname{re}(x) \le \operatorname{re}(y) $$$

Lean4

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

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

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

Разделы

Аффилиация

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