isClosed_range_intCast

Mathlib.Analysis.Complex.Basic

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

English

The range of Int.cast: ℤ → ℂ is a closed subset of ℂ.

Русский

Область значений Int.cast: ℤ → ℂ содержит замкнутое множество в ℂ.

LaTeX

$$$IsClosed( Set.range (Int.cast) )$$$

Lean4

theorem isClosed_range_intCast : IsClosed (Set.range ((↑) : ℤ → ℂ)) :=
  Complex.closedEmbedding_intCast.isClosed_range

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

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

Разделы

Аффилиация

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