inclusion

Mathlib.Topology.Constructions

URI: https://scilib.ai/kg/mathlib#Topology.IsEmbedding.inclusion

English

If s ⊆ t, the inclusion map from s into t is an embedding.

Русский

Если s ⊆ t, то включение s в t является вложением.

LaTeX

$$$\\forall s\\subseteq t,\\; \\text{IsEmbedding}(\\text{inclusion}(s\\subseteq t)).$$$

Lean4

protected theorem inclusion (h : s ⊆ t) : IsEmbedding (inclusion h) :=
  IsEmbedding.subtypeVal.codRestrict _ _

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

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

Разделы

Аффилиация

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