instPerfectSpace

Mathlib.Topology.Algebra.Module.PerfectSpace

URI: https://scilib.ai/kg/mathlib#instPerfectSpace

English

There is an instance giving 𝕜 as a perfect space whenever the hypotheses hold.

Русский

Существует экземпляр, наделяющий 𝕜 свойством совершенного пространства при выполнении условий.

LaTeX

$$$\text{instance: PerfectSpace } 𝕜$$$

Lean4

instance : PerfectSpace 𝕜 :=
  perfectSpace_of_module 𝕜 𝕜

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

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

Разделы

Аффилиация

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