eventuallyEq_one

Mathlib.Topology.PartitionOfUnity

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

English

There exists i with f_i(x) eventually equal to 1 at nhds x.

Русский

Существует i такой, что f_i(x) эквивалентно 1 ближе к nhds x.

LaTeX

$$$$ \exists i, f_i(x) = 1 \text{ eventually as } x \to x. $$$$

Lean4

theorem eventuallyEq_one (x : X) (hx : x ∈ s) : f (f.ind x hx) =ᶠ[𝓝 x] 1 :=
  (f.eventuallyEq_one' x hx).choose_spec

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

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

Разделы

Аффилиация

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