injective

Mathlib.Analysis.Normed.Operator.Conformal

URI: https://scilib.ai/kg/mathlib#IsConformalMap.injective

← MathLib Explorer

English

If f is conformal, then f is injective.

Русский

Если отображение конформно, то оно инъективно.

LaTeX

$$$IsConformalMap f\Rightarrow Function.Injective f$$$

Lean4

protected theorem injective {f : M' →L[R] N} (h : IsConformalMap f) : Function.Injective f :=
  by
  rcases h with ⟨c, hc, li, rfl⟩
  exact (smul_right_injective _ hc).comp li.injective

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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