filterAt_basis_closedBall — Mathlib

English

The filter at x has a basis indexed by radii ε > 0 with sets t ∈ v.setsAt x and t ⊆ closedBall(x, ε).

Русский

Фильтр в x имеет базис, индексируемый по ε>0, состоящий из t ∈ v.setsAt(x) с t ⊆ closedBall(x, ε).

LaTeX

$$$(v.filterAt x).HasBasis(\\lambda ε, ε>0) (\\lambda ε, \\{t\\in v.setsAt x \\mid t\\subseteq \\overline{B}(x, ε)\\}).$$$

Lean4

theorem filterAt_basis_closedBall (x : X) : (v.filterAt x).HasBasis (0 < ·) ({t ∈ v.setsAt x | t ⊆ closedBall x ·}) :=
  nhds_basis_closedBall.vitaliFamily v

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