lim_re

Mathlib.Analysis.Complex.Norm

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

English

The real part of the limit equals the limit of the real parts: lim (cauSeqRe f) = Re(lim f).

Русский

Действительная часть предела равна пределу действительных частей: lim (cauSeqRe f) = Re(lim f).

LaTeX

$$$\\lim (cauSeqRe f) = \\operatorname{Re}(\\lim f)$$$

Lean4

theorem lim_re (f : CauSeq ℂ (‖·‖)) : lim (cauSeqRe f) = (lim f).re := by rw [lim_eq_lim_im_add_lim_re]; simp [ofReal]

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

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

Разделы

Аффилиация

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