hasBasis_cobounded_norm'

Mathlib.Analysis.Normed.Group.Bounded

URI: https://scilib.ai/kg/mathlib#Filter.hasBasis_cobounded_norm'

← MathLib Explorer

English

The cobounded filter has a basis labeled by true and thresholds {x | ∥x∥ ≤ t}.

Русский

cobounded имеет базис с порогами {x : ∥x∥ ≤ t}.

LaTeX

$$HasBasis (cobounded E) (fun _ => True) ({x | ∥x∥ ≤ r})$$

Lean4

@[to_additive Filter.hasBasis_cobounded_norm]
theorem hasBasis_cobounded_norm' : HasBasis (cobounded E) (fun _ ↦ True) ({x | · ≤ ‖x‖}) :=
  atTop_basis.cobounded_of_norm'

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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