lim_im

Mathlib.Analysis.Complex.Norm

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

English

The imaginary part of the limit equals the limit of the imaginary parts: lim (cauSeqIm f) = Im(lim f).

Русский

Мнимая часть предела равна пределу мнимых частей: lim (cauSeqIm f) = Im(lim f).

LaTeX

$$$\\lim (cauSeqIm f) = \\operatorname{Im}(\\lim f)$$$

Lean4

theorem lim_im (f : CauSeq ℂ (‖·‖)) : lim (cauSeqIm f) = (lim f).im := by rw [lim_eq_lim_im_add_lim_re]; simp [ofReal]

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

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

Разделы

Аффилиация

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