continuous_inclusion

Mathlib.Topology.Constructions

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

English

If S ⊆ T are subsets of a space X, then the inclusion map i: S → T is continuous.

Русский

Если S ⊆ T ⊆ X, то включение i: S → T непрерывно.

LaTeX

$$$\text{Continuous}(\iota: S \hookrightarrow T)$ where $\iota(x)=x$ for $x\in S$ and $S\subseteq T$.$$

Lean4

theorem continuous_inclusion {s t : Set X} (h : s ⊆ t) : Continuous (inclusion h) :=
  continuous_id.subtype_map h

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

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

Разделы

Аффилиация

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