eq_lim_of_const_equiv

Mathlib.Algebra.Order.CauSeq.Completion

URI: https://scilib.ai/kg/mathlib#CauSeq.eq_lim_of_const_equiv

← MathLib Explorer

English

If CauSeq.const abv x is equivalent to f, then lim f = x.

Русский

Если константная последовательность CauSeq const abv x эквивалентна f, тогда lim f = x.

LaTeX

$$$\\text{If }\\ CauSeq.const(abv)\\; x \\approx f \\Rightarrow \\lim f = x$$$

Lean4

theorem eq_lim_of_const_equiv {f : CauSeq β abv} {x : β} (h : CauSeq.const abv x ≈ f) : x = lim f :=
  const_equiv.mp <| Setoid.trans h <| equiv_lim f

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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