instCompactSpace

Mathlib.Analysis.Complex.Circle

URI: https://scilib.ai/kg/mathlib#Circle.instCompactSpace

English

The circle is a compact space (as a subspace of the complex plane).

Русский

Окружность компактна как подпространство комплексной плоскости.

LaTeX

$$$$ Circle \\text{ is a CompactSpace} \\;.$$$$

Lean4

instance : CompactSpace Circle :=
  Metric.sphere.compactSpace _ _

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

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

Разделы

Аффилиация

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