conditional — Mathlib

English

The conditional summation filter on β is defined by taking finite intervals [p1, p2] via Finset.Icc and pushing forward by p ↦ Finset.Icc p1 p2 from atBot × atTop.

Русский

Условный фильтр суммирования на β задаётся образом конечных интервалов [p1,p2] через Finset.Icc и отображением p ↦ Finset.Icc p1 p2 из x×y.

LaTeX

$$$\\text{conditional }\\beta\\;\\text{defined by }\\text{filter}= (atBot \\times\\! atTop).map (\\lambda p, Finset.Icc(p.1,p.2))$$$

Lean4

/-- **Conditional summation**, for ordered types `β` such that closed intervals `[x, y]` are
finite: this corresponds to limits of finite sums over larger and larger intervals. -/
@[simps]
def conditional : SummationFilter β where filter := (atBot ×ˢ atTop).map (fun p ↦ Finset.Icc p.1 p.2)

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