map_specializes

Mathlib.Topology.ContinuousMap.Basic

URI: https://scilib.ai/kg/mathlib#ContinuousMap.map_specializes

English

If x specializes to y in α and f: α → β is continuous, then f(x) specializes to f(y) in β.

Русский

Если x специализируется на y в α и f: α → β непрерывна, то f(x) специализируется на f(y) в β.

LaTeX

$$$x \\!\\sSpecializes\\! y \\Rightarrow f(x) \\!\\sSpecializes\\! f(y)$ for continuous f$$

Lean4

theorem map_specializes (f : C(α, β)) {x y : α} (h : x ⤳ y) : f x ⤳ f y :=
  h.map f.2

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

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

Разделы

Аффилиация

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