map

Mathlib.Topology.Inseparable

URI: https://scilib.ai/kg/mathlib#Inseparable.map

English

If x ~ᵢ y and f is continuous, then f(x) ~ᵢ f(y).

Русский

Если x ~ᵢ y и f — непрерывно, то f(x) ~ᵢ f(y).

LaTeX

$$$(h : x \\sim_i y) \\to (Continuous f) \\Rightarrow f(x) \\sim_i f(y).$$$

Lean4

theorem map (h : x ~ᵢ y) (hf : Continuous f) : f x ~ᵢ f y :=
  h.map_of_continuousAt hf.continuousAt hf.continuousAt

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

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

Разделы

Аффилиация

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