extend_eq_at

Mathlib.Topology.DenseEmbedding

URI: https://scilib.ai/kg/mathlib#IsDenseInducing.extend_eq_at

← MathLib Explorer

English

If f is continuous at a, then di.extend f (i a) = f a.

Русский

Если f непрерывна в a, то di.extend f (i a) = f a.

LaTeX

$$$\\text{extend\_eq\_at }(di)(f)(a) : di.extend f (i a) = f a$$$

Lean4

theorem extend_eq_at [T2Space γ] (di : IsDenseInducing i) {f : α → γ} {a : α} (hf : ContinuousAt f a) :
    di.extend f (i a) = f a :=
  extend_eq_of_tendsto _ <| di.nhds_eq_comap a ▸ hf

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

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

Разделы

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

Аффилиация

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