outCLM_injective

Mathlib.Topology.Algebra.SeparationQuotient.Section

URI: https://scilib.ai/kg/mathlib#SeparationQuotient.outCLM_injective

English

outCLM is injective.

Русский

outCLM инъективен.

LaTeX

$$$\mathrm{outCLM}\,K\,E\;\text{injective}$$$

Lean4

theorem outCLM_injective : Function.Injective (outCLM K E) :=
  (isEmbedding_outCLM K E).injective

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

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

Разделы

Аффилиация

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