tendsto

Mathlib.Order.Filter.Tendsto

URI: https://scilib.ai/kg/mathlib#Set.MapsTo.tendsto

English

If h maps s to t, then Tendsto f (principal s) (principal t).

Русский

Если h отображает s в t, тогда Tendsto f (principal s) (principal t).

LaTeX

$$$ \\operatorname{MapsTo} f s t \\Rightarrow \\operatorname{Tendsto} f (\\mathcal{P} s) (\\mathcal{P} t) $$$

Lean4

theorem tendsto {s : Set α} {t : Set β} {f : α → β} (h : MapsTo f s t) : Filter.Tendsto f (𝓟 s) (𝓟 t) :=
  Filter.tendsto_principal_principal.2 h

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

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

Разделы

Аффилиация

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