const

Mathlib.Order.Filter.EventuallyConst

URI: https://scilib.ai/kg/mathlib#Filter.EventuallyConst.const

English

Constant function is EventuallyConst along any filter l.

Русский

Постоянная функция вдоль любого фильтра является EventuallyConst.

LaTeX

$$$\forall c,\ \mathrm{EventuallyConst}(\lambda x. c, l)$$$

Lean4

@[simp]
protected theorem const (c : β) : EventuallyConst (fun _ ↦ c) l :=
  .of_tendsto tendsto_const_pure

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

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

Разделы

Аффилиация

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