cobounded_neBot

Mathlib.Analysis.Normed.Module.Basic

URI: https://scilib.ai/kg/mathlib#NontriviallyNormedField.cobounded_neBot

English

If 𝕜 is a nontrivially normed field, then the cobounded filter on 𝕜 is nontrivial.

Русский

Если 𝕜 — ненулевое нормированное поле, то кобондированная фильтрация на 𝕜 не тривиальна.

LaTeX

$$$\\operatorname{NeBot}(\\operatorname{cobounded} 𝕜)$$$

Lean4

instance (priority := 100) cobounded_neBot : NeBot (cobounded 𝕜) :=
  NormedSpace.cobounded_neBot 𝕜 𝕜

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

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

Разделы

Аффилиация

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