eventually_eq

Mathlib.Topology.LocallyConstant.Basic

URI: https://scilib.ai/kg/mathlib#IsLocallyConstant.eventually_eq

English

The eventually-equal property: hf.eventually_eq x holds for every x.

Русский

Свойство eventually_eq: hf.eventually_eq x выполняется для каждого x.

LaTeX

$$$\\forall x, \\text{Eventually}(f(y) = f(x)) \\; (nhds(x))$$$

Lean4

protected theorem eventually_eq {f : X → Y} (hf : IsLocallyConstant f) (x : X) : ∀ᶠ y in 𝓝 x, f y = f x :=
  (iff_eventually_eq f).1 hf x

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

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

Разделы

Аффилиация

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