of_subsingleton

Mathlib.Topology.Maps.Basic

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

English

If X is subsingleton, any map f : X → Y is an embedding.

Русский

Если X — субоднос, любое отображение f: X → Y является вложением.

LaTeX

$$$[\text{Subsingleton } X] \; (f : X\to Y) \Rightarrow \mathrm{IsEmbedding}(f)$$$

Lean4

theorem of_subsingleton [Subsingleton X] (f : X → Y) : IsEmbedding f :=
  ⟨.of_subsingleton f, f.injective_of_subsingleton⟩

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

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

Разделы

Аффилиация

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