finsupport — Mathlib

English

Finsupport at a point x0 is the set of indices i with x0 in the support of f_i.

Русский

Finsupport в точке x0 — множество индексов i, таких что x0 принадлежит опоре f_i.

LaTeX

$$$\text{finsupport}_{x_0} = \{ i \mid x_0 \in \operatorname{supp}(f_i)\}$$$

Lean4

/-- The support of a partition of unity at a point `x₀` as a `Finset`.
  This is the set of `i : ι` such that `x₀ ∈ support f i`, i.e. `f i ≠ x₀`. -/
def finsupport : Finset ι :=
  (ρ.locallyFinite.point_finite x₀).toFinset

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