injective

Mathlib.Topology.MetricSpace.DilationEquiv

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

English

A DilationEquiv map e is injective.

Русский

отображение e инъективно.

LaTeX

$$$\forall e : X \simeq^{\mathrm{d}} Y,\ Injective (e)$$$

Lean4

protected theorem injective (e : X ≃ᵈ Y) : Injective e :=
  e.1.injective

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

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

Разделы

Аффилиация

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