finInit

Mathlib.Topology.Constructions

URI: https://scilib.ai/kg/mathlib#ContinuousAt.finInit

← MathLib Explorer

English

If f is continuous at x, then a ↦ Fin.init (f a) is continuous at x.

Русский

Если f непрерывна в x, то a ↦ Fin.init(f(a)) непрерывна в x.

LaTeX

$$$\\displaystyle \\text{ContinuousAt}\\bigl( a \\mapsto \\mathrm{Fin.init}( f(a) ) \\bigr)\\; x.$$$

Lean4

@[fun_prop]
theorem finInit {f : X → ∀ j : Fin (n + 1), A j} {x : X} (hf : ContinuousAt f x) :
    ContinuousAt (fun a ↦ Fin.init (f a)) x :=
  hf.tendsto.finInit

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

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

Разделы

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

Аффилиация

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