map_coe

Mathlib.Topology.UniformSpace.AbstractCompletion

URI: https://scilib.ai/kg/mathlib#AbstractCompletion.map_coe

English

For any a in α, the image of ι a under map f equals ι'(f a).

Русский

Для каждого a ∈ α образ ι a под отображением map f совпадает с ι'(f a).

LaTeX

$$$ \forall a:\alpha,\ map f (ι a) = ι' (f a) $$$

Lean4

@[simp]
theorem map_coe (hf : UniformContinuous f) (a : α) : map f (ι a) = ι' (f a) :=
  pkg.extend_coe (pkg'.uniformContinuous_coe.comp hf) a

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

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

Разделы

Аффилиация

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