uniformly_extend_of_ind

Mathlib.Topology.UniformSpace.UniformEmbedding

URI: https://scilib.ai/kg/mathlib#uniformly_extend_of_ind

English

For b in β, ψ(e(b)) = f(b); the extension agrees with the original on the image of e.

Русский

Для b в β, ψ(e(b)) = f(b); продолжение совпадает с исходной функцией на образе e.

LaTeX

$$$\psi( e(b) ) = f(b)\quad( b\in β )$$$

Lean4

theorem uniformly_extend_of_ind (b : β) : ψ (e b) = f b :=
  IsDenseInducing.extend_eq_at _ h_f.continuous.continuousAt

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

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

Разделы

Аффилиация

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