ind

Mathlib.Topology.PartitionOfUnity

URI: https://scilib.ai/kg/mathlib#BumpCovering.ind

English

Index of a bump i such that fs_i =ᶠ[𝓝 x] 1

Русский

Индекс таков, что f_i(x) близко к 1 в nhds x.

LaTeX

$$$$ \text{ind}(x) \in \iota \text{ with } f_{\text{ind}(x)}(x) = 1 \text{ eventually.} $$$$

Lean4

/-- Index of a bump function such that `fs i =ᶠ[𝓝 x] 1`. -/
def ind (x : X) (hx : x ∈ s) : ι :=
  (f.eventuallyEq_one' x hx).choose

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru