hasBasis_nhds_zero

Mathlib.Topology.Algebra.Valued.ValuativeRel

URI: https://scilib.ai/kg/mathlib#IsValuativeTopology.hasBasis_nhds_zero

← MathLib Explorer

English

Variant of the zero basis: (nhds 0).HasBasis (γ ≠ 0) ({ x | v x < γ }).

Русский

Вариант базиса нуля: (nhds 0).HasBasis (γ ≠ 0) ({ x | v x < γ }).

LaTeX

$$(nhds 0).HasBasis (γ ≠ 0) ({ x ∈ R | v x < γ })$$

Lean4

theorem hasBasis_nhds_zero : (𝓝 (0 : R)).HasBasis (fun _ => True) fun γ : (ValueGroupWithZero R)ˣ => {x | v x < γ} := by
  convert hasBasis_nhds (0 : R); rw [sub_zero]

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

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

Разделы

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

Аффилиация

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