filterAt — Mathlib

English

The filter at x is defined as the infimum of the neighborhood filter and the principal filter generated by setsAt x.

Русский

Фильтр в точке x есть инфиминум соседствующего фильтра и принциального фильтра, порожденного setsAt x.

LaTeX

$$$\\text{filterAt}(x) = (\\mathcal{N}(x)\\text{ smallSets})\\inf (\\mathcal{P}(v.setsAt x)).$$$

Lean4

/-- Given a vitali family `v`, then `v.filterAt x` is the filter on `Set X` made of those families
that contain all sets of `v.setsAt x` of a sufficiently small diameter. This filter makes it
possible to express limiting behavior when sets in `v.setsAt x` shrink to `x`. -/
def filterAt (x : X) : Filter (Set X) :=
  (𝓝 x).smallSets ⊓ 𝓟 (v.setsAt x)

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