topology — Mathlib

English

The topology associated to a ring filter basis is defined by taking the underlying additive-group topology induced by BR; i.e., the topology on R is BR.topology.

Русский

Топология, связанная с кольцевой фильтр-базой, задаётся через топологию аддитивной группы BR; то есть топология на R равна BR.topology.

LaTeX

$$$\text{topology}(R) = BR.toAddGroupFilterBasis.topology$.$$

Lean4

/-- The topology associated to a ring filter basis.
It has the given basis as a basis of neighborhoods of zero. -/
def topology : TopologicalSpace R :=
  B.toAddGroupFilterBasis.topology

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