subtypeVal

Mathlib.Topology.Constructions

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

English

The inclusion map from the subtype p into Y is an embedding.

Русский

Включение из подтипа p в Y является вложением (эмбеддингом).

LaTeX

$$$$ \\text{IsEmbedding}((\\uparrow):\\text{Subtype}(p)\\to Y). $$$$

Lean4

theorem subtypeVal : IsEmbedding ((↑) : Subtype p → X) :=
  ⟨.subtypeVal, Subtype.coe_injective⟩

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

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

Разделы

Аффилиация

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